| | 56 | == Deliverables == |
| | 57 | |
| | 58 | === Organization === |
| | 59 | |
| | 60 | * [R01] Roadmap of the project |
| | 61 | * [R02] Annual report 1 |
| | 62 | * [R03] Annual report 2 |
| | 63 | * [R04] Annual report 3 |
| | 64 | * [R05] Final report |
| | 65 | |
| | 66 | === Task 1 === |
| | 67 | |
| | 68 | * [S05] Definition of New Nestable Algorithmic Skeletons |
| | 69 | * [P06] Research report about "Definition of new algorithmic skeletons" |
| | 70 | * [S07] Proof of Algorithmic Skeletons |
| | 71 | * [P08] Research report about "Proving algorithmic skeletons in Coq" |
| | 72 | * [S09] Coq library for deriving parallel programs with algorithmic skeletons |
| | 73 | * [P10] Research report about "Derivation of parallel programs in Coq" |
| | 74 | * [S11] Some example applications with current definition of skeletons |
| | 75 | * [S12] Further example applications with full set of algorithmic skeletons |
| | 76 | * [P13] Research report about "Example applications developed with algorithmic skeletons and their derivation from specification" |
| | 77 | |
| | 78 | === Task 2 === |
| | 79 | |
| | 80 | * [S14] Release of the !SkeTo Library version 1.X |
| | 81 | * [S15] Release of the OSL Library version 1.Y |
| | 82 | * [P16] Report “Efficient C++ MetaProgrammed Algorithmic Skeleton Libraries” |
| | 83 | * [S17] Release of the !SkeTo Library version 1.X' |
| | 84 | * [S18] Release of the OSL Library version 1.Y' |
| | 85 | * [P19] Report “Hybrid Parallelism in C++ Algorithmic Skeleton Libraries” |
| | 86 | * [S20] Release of a set of example applications for !SkeTo and OSL |
| | 87 | * [P21] Report “Efficient Parallel Programming with !SkeTo and OSL” |
| | 88 | * [S22] A Formal Semantics for !SkeTo and OSL in Coq: [http://frederic.loulergue.eu/ftp/OSLSemantics-0.1.tar.bz2 v0.1], [http://frederic.loulergue.eu/ftp/OSLSemantics-0.2.tar.bz2 v0.2] |
| | 89 | * [P23] Report "A Formal Semantics for !SkeTo and OSL in Coq" |
| | 90 | * [S24] A Verified Library of Algorithmic Skeletons: v1.0 (coming soon) |
| | 91 | * [P25] Report "[http://traclifo.univ-orleans.fr/PaPDAS/raw-attachment/wiki/deliverable_p25.pdf A Verified Library of Algorithmic Skeletons]" |
| | 92 | |
| | 93 | === Task 3 === |
| | 94 | |
| | 95 | * [P26] Report “Definition and mechanization of ASC semantics” |
| | 96 | * [P27] Report “Extraction of skeleton based specifications” |
| | 97 | * [S28] Coq code for ASC and tool for extraction of ASC programs |
| | 98 | * ''[S29] Cancelled'' |
| | 99 | * ''[P30] Cancelled'' |
| | 100 | * [P31] Report "Mechanized distributed semantics of C-light+TCP/IP" |
| | 101 | * [P32] Report “Compiling ASC into C-light+TCP/IP” |
| | 102 | * [S33] !CompCert x86-TCP/IP |
| | 103 | * [P34] Report "!CompCert x86-TCP/IP" |
| | 104 | * [P35] Report "Mechanized semantics of C-light-MT" |
| | 105 | * [P36] Report "Compiling ASC into C-light-MT" |
| | 106 | * [S37] CompCert x86MT |
| | 107 | * [P38] Report "CompCert x86MT" |
| | 108 | |
