Skip to content

Commit 18c5810

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

7 files changed

Lines changed: 146 additions & 8 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:

‎.github/scripts/record_model_state_space.py‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
from argparse import ArgumentParser
77
import logging
8-
from os.path import dirname, normpath
8+
from os.path import dirname, normpath, join
99
from subprocess import CompletedProcess, TimeoutExpired
1010
import tla_utils
1111

@@ -96,7 +96,7 @@ def check_model(module, model):
9696
or 'stateDepth' not in model
9797
))
9898
],
99-
key = lambda m: m[2],
99+
key = lambda m: m[3],
100100
reverse=True
101101
)
102102

@@ -108,7 +108,7 @@ def check_model(module, model):
108108
success = check_model(module, model)
109109
if not success:
110110
exit(1)
111-
tla_utils.write_json(manifest, manifest_path)
111+
tla_utils.write_json(spec, manifest_path)
112112

113113
exit(0)
114114

‎.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: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
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+
"distinctStates": 64,
26+
"totalStates": 194,
27+
"stateDepth": 7
28+
}
29+
]
30+
},
31+
{
32+
"path": "specifications/barriers/Barriers.tla",
33+
"communityDependencies": [],
34+
"tlaLanguageVersion": 2,
35+
"features": [
36+
"pluscal",
37+
"proof"
38+
],
39+
"models": [
40+
{
41+
"path": "specifications/barriers/Barriers.cfg",
42+
"runtime": "00:00:05",
43+
"size": "small",
44+
"mode": "exhaustive search",
45+
"result": "success",
46+
"distinctStates": 29279,
47+
"totalStates": 104515,
48+
"stateDepth": 93
49+
}
50+
]
51+
}
52+
]
53+
}

‎specifications/locks_auxiliary_vars/manifest.json‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
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+
"distinctStates": 12,
29+
"totalStates": 21,
30+
"stateDepth": 5
31+
}
32+
]
33+
},
34+
{
35+
"path": "specifications/locks_auxiliary_vars/LockHS.tla",
36+
"communityDependencies": [],
37+
"tlaLanguageVersion": 2,
38+
"features": [
39+
"proof"
40+
],
41+
"models": [
42+
{
43+
"path": "specifications/locks_auxiliary_vars/LockHS.cfg",
44+
"runtime": "00:00:01",
45+
"size": "small",
46+
"mode": "exhaustive search",
47+
"result": "success",
48+
"distinctStates": 28,
49+
"totalStates": 41,
50+
"stateDepth": 10
51+
}
52+
]
53+
},
54+
{
55+
"path": "specifications/locks_auxiliary_vars/Peterson.tla",
56+
"communityDependencies": [],
57+
"tlaLanguageVersion": 2,
58+
"features": [
59+
"pluscal",
60+
"proof"
61+
],
62+
"models": [
63+
{
64+
"path": "specifications/locks_auxiliary_vars/Peterson.cfg",
65+
"runtime": "00:00:01",
66+
"size": "small",
67+
"mode": "exhaustive search",
68+
"result": "success",
69+
"distinctStates": 42,
70+
"totalStates": 77,
71+
"stateDepth": 11
72+
}
73+
]
74+
},
75+
{
76+
"path": "specifications/locks_auxiliary_vars/Stuttering.tla",
77+
"communityDependencies": [],
78+
"tlaLanguageVersion": 2,
79+
"features": [],
80+
"models": []
81+
}
82+
]
83+
}

0 commit comments

Comments
 (0)