| | 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" |
| | 147 | |
| | 148 | |
