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