Commit efdccc00 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Created new README.

parent 09bf90db
# Pirouette: Typed Functional Choreographies
## Getting The Code
You can find this via MPI-SWS Gitlab instance at https://gitlab.mpi-sws.org/akhirsch/pirouette-coq
## Mapping from Theorems in the Paper to Code
The equations for substitutions required for local programs can be found in LocalLang.v.
Likewise, the required-admissable rules for type systems can be found in TypedLocalLang.v.
| Theorem Name (From Paper) | Theorem Number (From Paper) | Coq File(s) | Coq Name(s) |
|-----------------------------|-----------------------------|---------------------------------------------------------|----------------------------------------------|
| Lambda Calculus Example | | LambdaCalc.v | |
| STLC Example | | STLC.v and STLCSound.v | |
| Natural-Numbers Example | | NatLang.vo, TypedNatLang.vo, and SoundlyTypedNatLang.vo | |
| Relative Preservation | Theorem 1 | TypedPirouette.v | RelativePreservation |
| Relative Progress | Theorem 2 | TypedPirouette.v | RelativeProgress |
| Relative Soundness | Corollary 1 | SoundlyTypedPirouette.v | Preverstion, StepsPreservation, and Progress |
| Equivalence Respects Types | Theorem 3 | TypedPirouette.v | EquivTyping |
| Operational Semantics Simulates Equivalence | Theorem 4 | Pirouette.v | EquivSimulation |
| Weak Semantics | Theorem 5 | RestrictedSemantics.v | StdToRStep and RStepToStd |
| Equivalence Begets Equality | Theorem 6 | EndPointProjection.v | EPPEquivToEq |
| Lifting System Steps | Theorem 7 (Part 1) | CtrlLang.v | LiftSystemNondetStep |
| Lowering System Steps | Theorem 7 (Part 2) | EndPointProjection.v | LowerCompiledSystemStep |
| Local Completeness | Theorem 8 | EndPointProjection.v | FullLocalCompleteness |
| Global Completeness | Theorem 9 | EndPointProjection.v | FullCompleteness |
| Local Soundness (Iota) | Theorem 10 (Part 1) | EndPointProjection.v | LocalIotaSoundness |
| Local Soundness (Comm) | Theorem 10 (Part 2) | EndPointProjection.v | LocalCommSoundness |
| Local Soundness (Sync) | Theorem 10 (Part 3) | EndPointProjection.v | LocalSyncSoundness |
| Local Soundness (SyncIota) | Theorem 10 (Part 4) | EndPointProjection.v | LocalSyncIotaSoundness |
| Global Soundness | Theorem 11 | EndPointProjection.v | Soundness |
| Deadlock Fredom by Design | Theorem 12 | EndPointProjection.v | DeadlockFreedomByDesign |
The following table refers to theorems found only in Appendix G of the technical-report version of the paper:
| Theorem Name (From Paper) | Theorem Number (From Paper) | Coq File(s) | Coq Name(s) |
|-----------------------------|-----------------------------|--------------------------------------------------------|----------------------------------------------|
| Pirouette Types Structural Rules | Theorem 13 | TypedPirouette.v | TypeLocalWeakening, TypePirExprWeakening and PirExprClosedAboveTyping |
| Equivalence Preserves Variables | Theorem 14 (Part 1) | Pirouette.v | PirExprClosedAboveEquiv |
| Equivalence Preserves Location Names | Theorem 14 (Part 2) | Pirouette.v | LocsInPirExprInvariant |
| Equivalence Preserves Values | Theorem 14 (Part 3) | Pirouette.v | PirExprValStableEquiv |
| Equivalence Preserves Local Substitution | Theorem 14 (Part 4) | Pirouette.v | EquivStableLocalSubst |
| Equivalence Preserves Global Substitution | Theorem 14 (Part 5) | Pirouette.v | WeakSubstExt |
| Merge is Idempotent | Theorem 15 (Part 1) | CtrlLanguage.v | MergeIdempotent |
| Merge is Commutative | Theorem 15 (Part 2) | CtrlLanguage.v | MergeComm |
| Merge is Associative | Theorem 15 (Part 3) | CtrlLanguage.v | MergeAssoc and MergeAssocNone |
| Merge Preserves Free Vars | Theorem 16 (Part 1) | CtrlLanguage.v | MergeClosed |
| Merge Preserves Local Substitution | Theorem 16 (Part 2) | CtrlLanguage.v | MergeExprSubst |
| Merge Preserves Global Substitution | Theorem 16 (Part 3) | CtrlLanguage.v | MergeSubst |
| Merge Preserves Values | Theorem 16 (Part 4) | CtrlLanguage.v | MergeCtrlExprVals and MergeRelToVal |
| Merge Preserves Reduction | Theorem 17 | CtrlLanguage.v | MergeStep' and MergeStep'Exists |
| Merge Creates Reduction | Theorem 17 | CtrlLanguage.v | UnmergeRelStep |
| EPP Preserves Variables | Theorem 18 (Part 1) | EndPointProjection.v | EPPClosedAbove |
| EPP Preserves Local Substitution | Theorem 18 (Part 2) | EndPointProjection.v | EPPLocalSubst |
| EPP Preserves Global Substitution | Theorem 18 (Part 3) | EndPointProjection.v | EPPSubst |
| EPP Preserves Values | Theorem 18 (Part 4) | EndPointProjection.v | EPPValue |
| EPP Creates Values | Theorem 18 (Part 5) | EndPointProjection.v | ValueSoundness |
| LND is Reflexive | Theorem 19 (Part 1) | CtrlLanguage.v | LessNondetRefl |
| LND is Antisymmetric | Theorem 19 (Part 2) | CtrlLanguage.v | LessNondetAntisym |
| LND is Transitive | Theorem 19 (Part 3) | CtrlLanguage.v | LessNondetTrans |
| LND Preserves Local Substitition | Theorem 20 (Part 1) | CtrlLanguage.v | LessNondetExprSubst |
| LND Preserves Global Substitition | Theorem 20 (Part 2) | CtrlLanguage.v | LessNondetSubst |
| Merging Creates LND | Thoerem 20 (Part 3) | CtrlLanguage.v | MergeLessNondet |
| Merging Preserves LND | Theorem 20 (Part 4) | CtrlLanguage.v | LessNondetMerge |
| LND is Reflexivity on Values | Theorem 20 (Part 5) | CtrlLanguage.v | LessNondetVals |
| Steps Lift Across LND | Theorem 21 | CtrlLanguage.v | LiftStepWithNondet |
| Lowering steps Across LND | Theorem 22 | CtrlLanguage.v | LowerStepNondet |
## Compiling
This has been tested with vanilla Coq 8.13.2.
To generate the makefile, type `coq_makefile -f Makefile -o _CoqProject`.
Then, you can simply type `make` in order to build the entire project, and `make clean` to remove compiled files.
In order to rebuild the makefile, type `coq_makefile -f Makefile -o _CoqProject` again.
Note that compiling takes a while, so get yourself a cup of coffee or something after typing `make`!
### Compile time
Sadly, `make` take quite a while.
In particular, several files (Pirouette.v, RestrictedSemantics.v, CtrlLang.v, and EndPointProjection.v) take several minutes to compile,
and both Pirouette.v and RestrictedSemantics.v take many minutes.
Here are the times per file, as reported by `make pretty-timed TIMING_REAL=1`:
| Time | Peak Mem | File Name |
|----------|-------------|--------------------------|
|41m09.94s | 17445240 ko | Total Time / Peak Mem |
|15m10.11s | 778832 ko | Pirouette.vo |
|14m00.01s | 763140 ko | RestrictedSemantics.vo |
| 6m53.25s | 17445240 ko | EndPointProjection.vo |
| 5m00.33s | 1195096 ko | CtrlLang.vo |
| 0m02.85s | 494208 ko | TypedPirouette.vo |
| 0m00.51s | 355152 ko | STLCSound.vo |
| 0m00.49s | 352468 ko | FunLMap.vo |
| 0m00.45s | 344880 ko | LambdaCalc.vo |
| 0m00.43s | 366200 ko | SoundlyTypedPirouette.vo |
| 0m00.31s | 346908 ko | STLC.vo |
| 0m00.22s | 266176 ko | TypedNatLang.vo |
| 0m00.20s | 221656 ko | NatLang.vo |
| 0m00.17s | 184740 ko | LocationMap.vo |
| 0m00.15s | 176296 ko | SoundlyTypedNatLang.vo |
| 0m00.15s | 166828 ko | UnitypedLC.vo |
| 0m00.08s | 82076 ko | LocalLang.vo |
| 0m00.07s | 71816 ko | TypedLocalLang.vo |
| 0m00.06s | 63984 ko | SoundlyTypedLocalLang.vo |
| 0m00.06s | 65832 ko | SyncLabels.vo |
| 0m00.05s | 61996 ko | Locations.vo |
## Size
This is a nontrivially large project.
It consists of 13,502 lines of Coq code in total.
Here is the breakdown of the lines of code as reported by `cloc --by-file-by-lang . --exclude-lang=make,D,Markdown`:
|File | blank | comment | code |
|---------------------------|-------|---------|-------|
| ./EndPointProjection.v | 139 | 123 | 3849 |
| ./CtrlLang.v | 204 | 257 | 3408 |
| ./Pirouette.v | 147 | 226 | 1825 |
| ./TreeLocationMap.v | 96 | 3 | 1604 |
| ./RestrictedSemantics.v | 31 | 66 | 567 |
| ./TypedPirouette.v | 31 | 77 | 456 |
| ./FunLMap.v | 54 | 16 | 455 |
| ./LambdaCalc.v | 41 | 52 | 323 |
| ./ListLMap.v | 44 | 107 | 152 |
| ./NatLang.v | 30 | 12 | 145 |
| ./STLC.v | 11 | 3 | 129 |
| ./LocationMap.v | 32 | 23 | 105 |
| ./UnitypedLC.v | 17 | 0 | 103 |
| ./TypedNatLang.v | 15 | 3 | 90 |
| ./LocalLang.v | 26 | 71 | 88 |
| ./STLCSound.v | 6 | 3 | 65 |
| ./TypedLocalLang.v | 16 | 58 | 51 |
| ./SoundlyTypedPirouette.v | 5 | 0 | 35 |
| ./SoundlyTypedNatLang.v | 5 | 0 | 30 |
| ./SoundlyTypedLocalLang.v | 3 | 9 | 12 |
| ./SyncLabels.v | 1 | 5 | 6 |
| ./Locations.v | 5 | 5 | 4 |
| SUM | 959 | 1119 | 13502 |
This has been tested with Coq 8.13.2. You shouldn't need any other libraries installed to use it.
Instructions to build:
coq_makefile -o Makefile -f _CoqProject
make
Then go get a cup of coffee! This takes about 30 minutes to build.
`cloc --by-file-by-lang . --exclude-lang=make,D`
72 text files.
classified 65 files 65 unique files.
92 files ignored.
github.com/AlDanial/cloc v 1.82 T=0.07 s (267.1 files/s, 231208.2 lines/s)
------------------------------------------------------------------------------------------
File blank comment code
------------------------------------------------------------------------------------------
./ChoreographyCompiler.v 184 335 4146
./ConcurrentLambda.v 225 964 3584
./Choreography.v 180 426 2002
./TreeLocationMap.v 96 3 1604
./RestrictedSemantics.v 34 29 575
./TypedChoreography.v 27 6 475
./LambdaCalc.v 48 60 408
./FunLMap.v 49 71 316
./STLC.v 14 0 161
./LocationMap.v 36 4 156
./NatLang.v 28 0 154
./TypedNatLang.v 18 0 123
./UnitypedLC.v 17 0 103
./TypedExpression.v 14 0 84
./Expression.v 14 23 81
./STLCSound.v 5 0 65
./SoundlyTypedChoreography.v 8 0 34
./SoundlyTypedNatLang.v 5 0 30
./SoundlyTypedExpression.v 3 0 14
./Locations.v 39 222 12
------------------------------------------------------------------------------------------
SUM: 1044 2143 14127
------------------------------------------------------------------------------------------
-------------------------------------------------------------------------------
Language files blank comment code
-------------------------------------------------------------------------------
Coq 20 1044 2143 14127
-------------------------------------------------------------------------------
SUM: 20 1044 2143 14127
-------------------------------------------------------------------------------
`make pretty-timed`
make[3]: Nothing to be done for 'real-all'.
Time | Peak Mem | File Name
-----------------------------------------------------
38m20.11s | 15898564 ko | Total Time / Peak Mem
-----------------------------------------------------
14m35.58s | 795940 ko | Choreography.vo
13m03.24s | 741840 ko | RestrictedSemantics.vo
5m46.46s | 15898564 ko | ChoreographyCompiler.vo
4m50.19s | 1120196 ko | ConcurrentLambda.vo
0m02.33s | 491104 ko | TypedChoreography.vo
0m00.37s | 355184 ko | STLCSound.vo
0m00.36s | 344856 ko | LambdaCalc.vo
0m00.32s | 439800 ko | FunLMap.vo
0m00.27s | 373508 ko | SoundlyTypedChoreography.vo
0m00.23s | 347044 ko | STLC.vo
0m00.15s | 275532 ko | TypedNatLang.vo
0m00.14s | 243072 ko | NatLang.vo
0m00.12s | 238792 ko | LocationMap.vo
0m00.09s | 167228 ko | UnitypedLC.vo
0m00.08s | 149712 ko | Locations.vo
0m00.07s | 176468 ko | SoundlyTypedNatLang.vo
0m00.05s | 78420 ko | Expression.vo
0m00.04s | 79696 ko | TypedExpression.vo
0m00.03s | 64208 ko | SoundlyTypedExpression.vo
`make pretty-timed TIMING_REAL=1`
make[3]: Nothing to be done for 'real-all'.
Time | Peak Mem | File Name
-----------------------------------------------------
38m26.06s | 15898564 ko | Total Time / Peak Mem
-----------------------------------------------------
14m35.88s | 795940 ko | Choreography.vo
13m03.55s | 741840 ko | RestrictedSemantics.vo
5m50.33s | 15898564 ko | ChoreographyCompiler.vo
4m50.53s | 1120196 ko | ConcurrentLambda.vo
0m02.48s | 491104 ko | TypedChoreography.vo
0m00.48s | 355184 ko | STLCSound.vo
0m00.47s | 344856 ko | LambdaCalc.vo
0m00.46s | 439800 ko | FunLMap.vo
0m00.37s | 373508 ko | SoundlyTypedChoreography.vo
0m00.29s | 347044 ko | STLC.vo
0m00.23s | 275532 ko | TypedNatLang.vo
0m00.21s | 243072 ko | NatLang.vo
0m00.20s | 238792 ko | LocationMap.vo
0m00.14s | 176468 ko | SoundlyTypedNatLang.vo
0m00.14s | 167228 ko | UnitypedLC.vo
0m00.12s | 149712 ko | Locations.vo
0m00.07s | 78420 ko | Expression.vo
0m00.07s | 79696 ko | TypedExpression.vo
0m00.05s | 64208 ko | SoundlyTypedExpression.vo
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment