| | 1 | === Organization (not publically available) === |
| | 2 | |
| | 3 | * '''[R01]''' Roadmap of the project |
| | 4 | * '''[R02]''' 6 months report |
| | 5 | * '''[R03]''' 18 months report |
| | 6 | * [R04] Final report |
| | 7 | |
| | 8 | === Task 1 === |
| | 9 | |
| | 10 | * [S05] Definition of New Nestable Algorithmic Skeletons |
| | 11 | * [P06] Research report about "Definition of new algorithmic skeletons" |
| | 12 | * [S07] Proof of Algorithmic Skeletons |
| | 13 | * [P08] Research report about "Proving algorithmic skeletons in Coq" |
| | 14 | * [S09] Coq library for deriving parallel programs with algorithmic skeletons |
| | 15 | * [P10] Research report about "Derivation of parallel programs in Coq" |
| | 16 | * [S11] Some example applications with current definition of skeletons |
| | 17 | * [S12] Further example applications with full set of algorithmic skeletons |
| | 18 | * [P13] Research report about "Example applications developed with algorithmic skeletons and their derivation from specification" |
| | 19 | |
| | 20 | === Task 2 === |
| | 21 | |
| | 22 | * [S14] Release of the !SkeTo Library version 1.5: [http://sketo.ipl-lab.org/archives/sketo-1.50pre.tar.gz SkeTo 1.5pre] |
| | 23 | * [S15] Release of the OSL Library version 1.0 |
| | 24 | * [P16] Report “Efficient C++ Meta-Programmed Algorithmic Skeleton Libraries” |
| | 25 | * [S17] Release of the !SkeTo Library version 2.0 |
| | 26 | * [S18] Release of the OSL Library version 1.5 |
| | 27 | * [P19] Report “Hybrid Parallelism in C++ Algorithmic Skeleton Libraries” |
| | 28 | * [S20] Release of a set of example skeletal applications |
| | 29 | * [P21] Report “Efficient Parallel Programming with BSP Homomorphism” |
| | 30 | * '''[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] |
| | 31 | * '''[P23]''' Report "[http://frederic.loulergue.eu/ftp/deliverable_p23.pdf Mechanised Semantics of an Algorithmic Skeleton Library]" |
| | 32 | * '''[S24]''' A Verified Library of Algorithmic Skeletons: [http://frederic.loulergue.eu/ftp/OSLPrototype-0.1.tar.gz v0.1] |
| | 33 | * '''[P25]''' Report "[http://frederic.loulergue.eu/ftp/deliverable_p25.pdf A Verified Library of Algorithmic Skeletons]" |
| | 34 | |
| | 35 | === Task 3 === |
| | 36 | |
| | 37 | * [P26] Report “Definition and mechanization of ASC semantics” |
| | 38 | * [P27] Report “Extraction of skeleton based specifications” |
| | 39 | * [S28] Coq code for ASC and tool for extraction of ASC programs |
| | 40 | * ''[S29] Cancelled'' |
| | 41 | * ''[P30] Cancelled'' |
| | 42 | * [P31] Report "Mechanized distributed semantics of C-light+TCP/IP" |
| | 43 | * [P32] Report “Compiling ASC into C-light+TCP/IP” |
| | 44 | * [S33] !CompCert x86-TCP/IP |
| | 45 | * [P34] Report "!CompCert x86-TCP/IP" |
| | 46 | * [P35] Report "Mechanized semantics of C-light-MT" |
| | 47 | * [P36] Report "Compiling ASC into C-light-MT" |
| | 48 | * [S37] !CompCert x86MT |
| | 49 | * [P38] Report "!CompCert x86MT" |
