| 94 | | |
| 95 | | == Deliverables == |
| 96 | | |
| 97 | | === Organization === |
| 98 | | |
| 99 | | * [R01] Roadmap of the project |
| 100 | | * [R02] Annual report #1 |
| 101 | | * [R03] Annual report #2 |
| 102 | | * [R04] Annual report #3 |
| 103 | | * [R05] Final report |
| 104 | | |
| 105 | | === Task 1 === |
| 106 | | |
| 107 | | * [S05] Definition of New Nestable Algorithmic Skeletons |
| 108 | | * [P06] Research report about "Definition of new algorithmic skeletons" |
| 109 | | * [S07] Proof of Algorithmic Skeletons |
| 110 | | * [P08] Research report about "Proving algorithmic skeletons in Coq" |
| 111 | | * [S09] Coq library for deriving parallel programs with algorithmic skeletons |
| 112 | | * [P10] Research report about "Derivation of parallel programs in Coq" |
| 113 | | * [S11] Some example applications with current definition of skeletons |
| 114 | | * [S12] Further example applications with full set of algorithmic skeletons |
| 115 | | * [P13] Research report about "Example applications developed with algorithmic skeletons and their derivation from specification" |
| 116 | | |
| 117 | | === Task 2 === |
| 118 | | |
| 119 | | * [S14] Release of the SkeTo Library version 1.5 |
| 120 | | * [S15] Release of the OSL Library version 1.0 |
| 121 | | * [P16] Report “Efficient C++ MetaProgrammed Algorithmic Skeleton Libraries” |
| 122 | | * [S17] Release of the SkeTo Library version 2 |
| 123 | | * [S18] Release of the OSL Library version 1.5 |
| 124 | | * [P19] Report “Hybrid Parallelism in C++ Algorithmic Skeleton Libraries” |
| 125 | | * [S20] Release of a set of example applications for SkeTo and OSL |
| 126 | | * [P21] Report “Efficient Parallel Programming with SkeTo and OSL” |
| 127 | | * [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] |
| 128 | | * [P23] Report "A Formal Semantics for SkeTo and OSL in Coq" |
| 129 | | * [S24] Verification of Metaprogrammed Optimization in C++ |
| 130 | | * [P25] Report "Verification of Metaprogrammed Optimization in C++" |
| 131 | | |
| 132 | | === Task 3 === |
| 133 | | |
| 134 | | * [P26] Report “Definition and mechanization of ASC semantics” |
| 135 | | * [P27] Report “Extraction of skeleton based specifications” |
| 136 | | * [S28] Coq code for ASC and tool for extraction of ASC programs |
| 137 | | * ''[S29] Cancelled'' |
| 138 | | * ''[P30] Cancelled'' |
| 139 | | * [P31] Report "Mechanized distributed semantics of C-light+TCP/IP" |
| 140 | | * [P32] Report “Compiling ASC into C-light+TCP/IP” |
| 141 | | * [S33] CompCert x86-TCP/IP |
| 142 | | * [P34] Report "CompCert x86-TCP/IP" |
| 143 | | * [P35] Report "Mechanized semantics of C-light-MT" |
| 144 | | * [P36] Report "Compiling ASC into C-light-MT" |
| 145 | | * [S37] CompCert x86MT |
| 146 | | * [P38] Report "CompCert x86MT" |
