Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Finitizing monotonic systems #97

Merged
merged 10 commits into from
Dec 1, 2023
Merged

Finitizing monotonic systems #97

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
72d0821
Added basic monotonic specs
ahelwer Oct 31, 2023
72d8aa7
Specs from blog post
ahelwer Oct 31, 2023
ed314a9
Constrained model
ahelwer Oct 31, 2023
1ad09f4
Added divergence based model
ahelwer Oct 31, 2023
b8707d1
CRDT spec finished
ahelwer Nov 1, 2023
1ce64cf
Wrote simple replicated log model
ahelwer Nov 1, 2023
5ac7778
Experiment with different GC methods
ahelwer Nov 1, 2023
e1e8edf
Added specs to manifest, added README
ahelwer Nov 22, 2023
a8bf6ba
Minor change to re-run CI
ahelwer Nov 22, 2023
bf9667d
Added blog post
ahelwer Nov 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 30 additions & 29 deletions README.md
View file
Open in desktop

Large diffs are not rendered by default.

212 changes: 152 additions & 60 deletions manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -389,6 +389,92 @@
}
]
},
{
"path": "specifications/FiniteMonotonic",
"title": "Finite Model-Checking of Monotonic Systems",
"description": "Illustration of technique for making ordinarily-infinite monotonic systems finite for the purposes of model-checking.",
"source": "https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/",
"authors": [
"Andrew Helwer"
],
"tags": [
"beginner"
ahelwer marked this conversation as resolved.
Show resolved Hide resolved
],
"modules": [
{
"path": "specifications/FiniteMonotonic/CRDT.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
},
{
"path": "specifications/FiniteMonotonic/MC_CRDT.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/FiniteMonotonic/MC_CRDT.cfg",
"runtime": "00:00:05",
"size": "small",
"mode": "exhaustive search",
"config": [],
"features": [
"liveness"
],
"result": "success"
}
]
},
{
"path": "specifications/FiniteMonotonic/MC_Constraint_CRDT.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg",
"runtime": "00:00:05",
"size": "small",
"mode": "exhaustive search",
"config": [],
"features": [
"liveness",
"state constraint"
],
"result": "success"
}
]
},
{
"path": "specifications/FiniteMonotonic/MC_ReplicatedLog.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/FiniteMonotonic/MC_ReplicatedLog.cfg",
"runtime": "00:00:05",
"size": "small",
"mode": "exhaustive search",
"config": [],
"features": [
"liveness"
],
"result": "success"
}
]
},
{
"path": "specifications/FiniteMonotonic/ReplicatedLog.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
}
]
},
{
"path": "specifications/GameOfLife",
"title": "Conway's Game of Life",
Expand Down Expand Up @@ -458,6 +544,22 @@
],
"tags": [],
"modules": [
{
"path": "specifications/KeyValueStore/ClientCentric.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
},
{
"path": "specifications/KeyValueStore/KVsnap.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [
"pluscal"
],
"models": []
},
{
"path": "specifications/KeyValueStore/KeyValueStore.tla",
"communityDependencies": [],
Expand Down Expand Up @@ -504,13 +606,6 @@
}
]
},
{
"path": "specifications/KeyValueStore/KVsnap.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": ["pluscal"],
"models": []
},
{
"path": "specifications/KeyValueStore/MCKVsnap.tla",
"communityDependencies": [],
Expand Down Expand Up @@ -539,13 +634,6 @@
"tlaLanguageVersion": 2,
"features": [],
"models": []
},
{
"path": "specifications/KeyValueStore/ClientCentric.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
}
]
},
Expand Down Expand Up @@ -770,6 +858,55 @@
}
]
},
{
"path": "specifications/Majority",
"title": "Boyer-Moore majority vote algorithm",
"description": "An efficient algorithm for detecting a majority value in a sequence",
"source": "",
"authors": [
"Stephan Merz"
],
"tags": [
"beginner"
],
"modules": [
{
"path": "specifications/Majority/MCMajority.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/Majority/MCMajority.cfg",
"runtime": "00:00:05",
"size": "small",
"mode": "exhaustive search",
"config": [
"ignore deadlock"
],
"features": [],
"result": "success"
}
]
},
{
"path": "specifications/Majority/Majority.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
},
{
"path": "specifications/Majority/MajorityProof.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [
"proof"
],
"models": []
}
]
},
{
"path": "specifications/MisraReachability",
"title": "Misra Reachability Algorithm",
Expand Down Expand Up @@ -3252,7 +3389,7 @@
"config": [
"ignore deadlock"
],
"features": [
"features": [
"liveness",
"state constraint",
"view"
Expand Down Expand Up @@ -3698,51 +3835,6 @@
"models": []
}
]
},
{
"path": "specifications/Majority",
"title": "Boyer-Moore majority vote algorithm",
"description": "An efficient algorithm for detecting a majority value in a sequence",
"source": "",
"authors": [
"Stephan Merz"
],
"tags": ["beginner"],
"modules": [
{
"path": "specifications/Majority/Majority.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": []
},
{
"path": "specifications/Majority/MCMajority.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/Majority/MCMajority.cfg",
"runtime": "00:00:05",
"size": "small",
"mode": "exhaustive search",
"config": ["ignore deadlock"],
"features": [],
"result": "success"
}
]
},
{
"path": "specifications/Majority/MajorityProof.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [
"proof"
],
"models": []
}
]
}
]
}
41 changes: 41 additions & 0 deletions specifications/FiniteMonotonic/CRDT.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
------------------------------- MODULE CRDT ---------------------------------

EXTENDS Naturals

CONSTANT Node

VARIABLE counter

TypeOK == counter \in [Node -> [Node -> Nat]]

Safety == \A n, o \in Node : counter[n][n] >= counter[o][n]

Monotonic == \A n, o \in Node : counter'[n][o] >= counter[n][o]

Monotonicity == [][Monotonic]_counter

Convergence == \A n, o \in Node : counter[n] = counter[o]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not a liveness property, but a state predicate on the initial state.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This just defines what it means for the system to have converged, there's a liveness property in Finitize_CRDT.tla with the definition Liveness == converge ~> S!Convergence.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The blog post stats that this is a liveness property:

Finally, the big one: this is an eventually-consistent system, so we want to validate its eventual consistency as a liveness property! We want to say it is always the case that eventually the vectors on all nodes will have the same value. Let’s define this goal state as:

https://github.com/tlaplus/Examples/pull/97/files#diff-9de53831fa4828bac3abea3e31ce96799638174ee08488d65cb5726b09113c3bR151-R155

If anything, the blog post has to be corrected. I presume the desired property would be \A n, o \in Node: []<>(counter[n] = counter[o]), combined with asserting fairness over Gossip.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It could be misread but it says it defines the "goal state" as that, not the liveness property generally

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"goal state" is rather ambiguous in a non-terminating system? At any rate, it seems easy to make less ambiguous.


Init == counter = [n \in Node |-> [o \in Node |-> 0]]

Increment(n) == counter' = [counter EXCEPT ![n][n] = @ + 1]

Gossip(n, o) ==
LET Max(a, b) == IF a > b THEN a ELSE b IN
counter' = [
counter EXCEPT ![o] = [
nodeView \in Node |->
Max(counter[n][nodeView], counter[o][nodeView])
]
]

Next ==
\/ \E n \in Node : Increment(n)
\/ \E n, o \in Node : Gossip(n, o)

Spec ==
/\ Init
/\ [][Next]_counter

=============================================================================

7 changes: 7 additions & 0 deletions specifications/FiniteMonotonic/MC_CRDT.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Node = {n1, n2, n3}
Divergence = 3
INVARIANTS TypeOK Safety
PROPERTIES Liveness Monotonicity

72 changes: 72 additions & 0 deletions specifications/FiniteMonotonic/MC_CRDT.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
------------------------------- MODULE MC_CRDT ------------------------------
ahelwer marked this conversation as resolved.
Show resolved Hide resolved

EXTENDS Naturals

CONSTANTS Node, Divergence

VARIABLES counter, converge

vars == <<counter, converge>>

S == INSTANCE CRDT

TypeOK ==
/\ S!TypeOK
/\ counter \in [Node -> [Node -> 0 .. Divergence]]
/\ converge \in BOOLEAN

Safety == S!Safety

Monotonicity == [][
\/ S!Monotonic
\/ \A a, b, c, d \in Node :
(counter'[a][b] - counter[a][b]) = (counter'[c][d] - counter[c][d])
]_vars

Liveness == converge ~> S!Convergence

Init ==
/\ S!Init
/\ converge = FALSE

Increment(n) ==
/\ ~converge
/\ counter[n][n] < Divergence
/\ S!Increment(n)
/\ UNCHANGED converge

Gossip(n, o) ==
/\ S!Gossip(n, o)
/\ UNCHANGED converge

Converge ==
/\ converge' = TRUE
/\ UNCHANGED counter

GarbageCollect ==
LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
LET Transpose == SetMin({counter[n][o] : n, o \in Node}) IN
/\ counter' = [
n \in Node |-> [
o \in Node |-> counter[n][o] - Transpose
]
]
/\ UNCHANGED converge

Next ==
\/ \E n \in Node : Increment(n)
\/ \E n, o \in Node : Gossip(n, o)
\/ Converge
\/ GarbageCollect

Fairness == \A n, o \in Node : WF_vars(Gossip(n, o))

StateConstraint == \A n, o \in Node : counter[n][o] <= 4

Spec ==
/\ Init
/\ [][Next]_vars
/\ Fairness

=============================================================================

6 changes: 6 additions & 0 deletions specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
SPECIFICATION Spec
CONSTANT Node = {n1, n2, n3}
INVARIANTS TypeOK Safety
PROPERTIES Monotonicity Liveness
CONSTRAINT StateConstraint

Loading