Skip to content

Commit 26d45e8

Browse files
ahelwerahelwer
committed
Added barrier and peterson's algorithm specs to CI
Specs were added in tlaplus#177 Signed-off-by: Andrew Helwer <ahelwer@pm.me>
1 parent 4414f33 commit 26d45e8

6 files changed

Lines changed: 128 additions & 5 deletions

File tree

‎.ciignore‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,3 @@ specifications/CCF
1111
specifications/azure-cosmos-tla
1212
specifications/microwave
1313

14-
# Basic contribution only
15-
specifications/barriers
16-
specifications/locks_auxiliary_vars

‎.github/scripts/check_proofs.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@
3131
for module in spec['modules']
3232
if 'proof' in module['features']
3333
and module['path'] not in skip_modules
34-
and (only_modules == [] or model['path'] in only_models)
34+
and (only_modules == [] or module['path'] in only_modules)
3535
]
3636

3737
for path in skip_modules:

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,9 @@
2121
## Don't ignore all folders
2222
!*/
2323

24+
## Don't ignore manifests
25+
!manifest.json
26+
2427
## Ignore TLAPS cache folder
2528
## See https://github.com/tlaplus/tlapm/issues/16
2629
__tlacache__

‎README.md‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,13 +48,16 @@ Here is a list of specs included in this repository which are validated by the C
4848
| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | |
4949
| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | |
5050
| [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | |
51+
| [Barrier Synchronization](specifications/barriers) | Jarod Differdange | | ✔ | ✔ | ✔ | |
52+
| [Peterson Lock Refinement With Auxiliary Variables](specifications/locks_auxiliary_vars) | Jarod Differdange | | ✔ | ✔ | ✔ | |
5153
| [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | |
5254
| [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe | | ✔ | (✔) | ✔ | |
5355
| [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | (✔) | | ✔ | |
5456
| [Asynchronous Reliable Broadcast](specifications/bcastByz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | | ✔ | |
5557
| [Distributed Mutual Exclusion](specifications/lamport_mutex) | Stephan Merz | | ✔ | | ✔ | |
5658
| [Two-Phase Handshaking](specifications/TwoPhase) | Leslie Lamport, Stephan Merz | | ✔ | | ✔ | |
5759
| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward) | Leslie Lamport | | (✔) | | ✔ | |
60+
| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer, Stephan Merz, Markus Kuppe | | ✔ | | ✔ | |
5861
| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | |
5962
| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | |
6063
| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | |
@@ -78,7 +81,6 @@ Here is a list of specs included in this repository which are validated by the C
7881
| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | |
7982
| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | |
8083
| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | |
81-
| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer, Stephan Merz, Markus Kuppe | | ✔ | | ✔ | |
8284
| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | |
8385
| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | |
8486
| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | |

‎specifications/barriers/manifest.json‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
{
2+
"path": "specifications/barriers",
3+
"title": "Barrier Synchronization",
4+
"description": "Barriers ensure a group of threads all reach the barrier before advancing",
5+
"sources": [
6+
"http://hdl.handle.net/2268.2/23374"
7+
],
8+
"authors": [
9+
"Jarod Differdange"
10+
],
11+
"tags": [],
12+
"modules": [
13+
{
14+
"path": "specifications/barriers/Barrier.tla",
15+
"communityDependencies": [],
16+
"tlaLanguageVersion": 2,
17+
"features": [],
18+
"models": [
19+
{
20+
"path": "specifications/barriers/Barrier.cfg",
21+
"runtime": "00:00:01",
22+
"size": "small",
23+
"mode": "exhaustive search",
24+
"result": "success"
25+
}
26+
]
27+
},
28+
{
29+
"path": "specifications/barriers/Barriers.tla",
30+
"communityDependencies": [],
31+
"tlaLanguageVersion": 2,
32+
"features": [
33+
"pluscal",
34+
"proof"
35+
],
36+
"models": [
37+
{
38+
"path": "specifications/barriers/Barriers.cfg",
39+
"runtime": "00:00:01",
40+
"size": "small",
41+
"mode": "exhaustive search",
42+
"result": "success"
43+
}
44+
]
45+
}
46+
]
47+
}

‎specifications/locks_auxiliary_vars/manifest.json‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
{
2+
"path": "specifications/locks_auxiliary_vars",
3+
"title": "Peterson Lock Refinement With Auxiliary Variables",
4+
"description": "Two-way refinement between Peterson's Algorithm and an abstract lock spec, using auxiliary variables as presented in *Prophecy made simple* by Lamport and Merz",
5+
"sources": [
6+
"http://hdl.handle.net/2268.2/23374"
7+
],
8+
"authors": [
9+
"Jarod Differdange"
10+
],
11+
"tags": [],
12+
"modules": [
13+
{
14+
"path": "specifications/locks_auxiliary_vars/Lock.tla",
15+
"communityDependencies": [],
16+
"tlaLanguageVersion": 2,
17+
"features": [
18+
"pluscal",
19+
"proof"
20+
],
21+
"models": [
22+
{
23+
"path": "specifications/locks_auxiliary_vars/Lock.cfg",
24+
"runtime": "00:00:01",
25+
"size": "small",
26+
"mode": "exhaustive search",
27+
"result": "success"
28+
}
29+
]
30+
},
31+
{
32+
"path": "specifications/locks_auxiliary_vars/LockHS.tla",
33+
"communityDependencies": [],
34+
"tlaLanguageVersion": 2,
35+
"features": [
36+
"proof"
37+
],
38+
"models": [
39+
{
40+
"path": "specifications/locks_auxiliary_vars/LockHS.cfg",
41+
"runtime": "00:00:01",
42+
"size": "small",
43+
"mode": "exhaustive search",
44+
"result": "success"
45+
}
46+
]
47+
},
48+
{
49+
"path": "specifications/locks_auxiliary_vars/Peterson.tla",
50+
"communityDependencies": [],
51+
"tlaLanguageVersion": 2,
52+
"features": [
53+
"pluscal",
54+
"proof"
55+
],
56+
"models": [
57+
{
58+
"path": "specifications/locks_auxiliary_vars/Peterson.cfg",
59+
"runtime": "00:00:01",
60+
"size": "small",
61+
"mode": "exhaustive search",
62+
"result": "success"
63+
}
64+
]
65+
},
66+
{
67+
"path": "specifications/locks_auxiliary_vars/Stuttering.tla",
68+
"communityDependencies": [],
69+
"tlaLanguageVersion": 2,
70+
"features": [],
71+
"models": []
72+
}
73+
]
74+
}

0 commit comments

Comments
 (0)