Some examples and notes while learning TLA+ modeling language.
-
TLA+
- Temporal Logic of Actions
- A logical formism based on simple math to describe systems
-
The mathematical model
- A behavior is a sequence of states
- A state is an assignment of values to variables
- The system is described by a formula about behaviors
- That's true on behaviors that represent possible system execution
- Usually obtained combining two formulas:
- Init to describe initial states
- Next to describe state transitions
Notes from Leslie Lamport Course
Lesson 1
- TLA+ is a language for high-level modeling of digital systems
- TLAPS, is the TLA+ proof system
- Use TLA+ to model criticla parts of digital systems
- Abstract away
- less critical parts
- lower-level implementation details
- TLA+ was designed for modeling concurrent and distributed systems
- Can help find and correct design errors
- errors hard to find by testing
- before writing any code
- Simplifying by removing details is called abstraction
- Only through abstraction can we understand complex systems
- We can't get systems right if we don't understand them
- Precise high-level models are called specifications
- TLA+ can specify algorithms and high-level designs
- You don't get a 10x reduction in code size by better coding, you get it by coming to a cleaner architecture
- An architecture is a higher-level specification - higher than the code level.
- We use TLA+ to ensure the systems we build work right
- Working right means satisfying certain properties
- The properties TLA+ can check are conditions on individual executions.
- An execution of a system is represented as a sequence of discrete steps.
- Digital system:
- We can abstract its continious evolution as a sequence of discrete events.
- We can simulate a concurrent system with a sequential program.
- TLA+ describes a step as a step change.
- An execution is represented as a sequence of states.
- A step is the change from one state to the next.
- TLA+ describes a state as an assignment of values to variables.
- A behavior is an infinite sequence of states
- An execution is represented as a behavior
- We want to specify all possible behaviors of a system
- A state machine is described by:
- All possible initial states.
- What next states can follow any given state.
- A state machine halts if there is no possible next state.
- In TLA+ a state machine is described by:
0. What the variables are.
- Possible initial values of variables.
- A relation between their values in the current state and their possible values in the next state.
Lesson 2
- We need precise language to describe state machines
- TLA+ uses ordinary, simple math
- Must replace AND (&&) by a mathimatical operator ∧ (logical AND)
- Must replace OR (||) by a mathimatical operator ∨ (logical OR)
- "i in {0,1,...,1000} is written as i ∈ 0..1000 in math
- In TLA+ we don't write instructions for computing something, we're writing a formula relating the values.
- The TLA+ source is in ASCII
- In ASCII, ∧ is typed as /\, ∨ is typed as \/ and ∈ is typed as \in
- The = sign in TLA+ means math equality, as in 2 + 2 = 4 unlike in most programming languages where it means assignment
- Math is much more expressive than standard programming language
- ∧ and ∨ are commutative, so interchaning groups in sub-formulas yields an equivalent formula.
- The math symbol ≜ means equal by definition. In TLA+ it is written as ==
Lesson 3
- Deadlock - Execution stopped when it wasn't supposed to.
- Termination - Execution stopped when it was suppose to. Most systems should not stop. The default is for TLC to regard stoppint as deadlock.
Lesson 4
- The best way to get started on a spec is to write a single correct behavior.
- TLA+ has no type declarations.
- Type correctness means all the variables have sensible values.
- We can define a formula that asserts type correctness. This helps readers understand the formula.
- TLC can check that type correctness is valid by checking the formula is always true.
- Names must be defined before they are used.
- A formula that is true in every reachable state is called an invariant
- The not equal operator is ≠ and is written in ASCII as /= or #
- ≤ is =< in TLA+ ASCII
- To keep things simple, use a primed variable v' only in one of these two kinds of formulas:
- v' = ... and v' ∈ ... where ... contains no primed variables
- comment out blocks with (* and *)
- ∃ means There is exists and is writen as \E in ASCII.
Lesson 5
- Use CONSTANT to declare a value that is the same throughout every behavior.
- In TLA+, every value is a set.
- Negation operator in C ! is ¬ in TLA+ and is written as ~ in ASCII
- TLA+ has two kinds of comments
- * an end of line comment"
-
(******************) (* boxed comments *) (* like this *) (******************)
- We can add pretty printed seperator lines with ---- in between statements
Lesson 6
- Records
- the definition
- r ≜ [prof |-> "Fred", num |-> 42]
- defines r to be a record with two fields prof and num.
- The values of it's two fields are
- r.prof = "Fred" and r.num = 42
- Chaning the order of the fields makes no difference
- r ≜ [prof |-> "Fred", num |-> 42]
- TLA+ format is
- [prof : {"Fred", "Ted", "Ned"}, num : 0..99]
- is the set of all records
- [prof |-> ..., num |-> ...]
- with prof field in set {"Fred", "Ted", "Ned"} and
- num field in set 0..99
- is the set of all records
- So [prof |-> "Ned", num |-> 24] is in this set.
- [prof : {"Fred", "Ted", "Ned"}, num : 0..99]
- This record is a function
- [prof |-> "Fred", num |-> 42]
- is a function f with domain {"prof", "num"}
- such that f["prof"] = "Fred" and f["num"] = 42
- [prof |-> "Fred", num |-> 42]
- f.prof is an abbreviation for f["prof"]
- This except expression equals the record that is the same as f except it's prof field is the string red
- [f EXCEPT !["prof"] = "Red"]
- this can be abbreviated as
- [f EXCEPT !.prof = "Red"]
- this can be abbreviated as
- [f EXCEPT !["prof"] = "Red"]
- the definition
- Subset ⊆ is written as \subseteq in ASCII and read is a subset of
- Union set operator ∪ is written as \union in ASCII S ∪ T is the set of all elements S or T or both
- UNCHANGED <<value1, value2, value3>> is equivalent to
^ value1' = value1 ^ value2' = value2 ^ value3' = value3
- Angle brackets ⟨ ⟩ is written as << >> in ASCII.
- The expression << >> is for ordered tuples.
- Enabling conditions should go before any prime action formulas.
Lesson 7
- CHOOSE v \in S : P equals
- if there is a v in S for which P is true
- then some such v
- else a completely unspecified value
- if there is a v in S for which P is true
- In math, any expression equals itself
- (CHOOSE i \in 1..99 : TRUE) = (CHOOSE i \in 1..9: TRUE)
- There is no nondetermism in a mathematical expression.
- x' \in 1..99
- Allows the value of x in the next state to be any number in 1..99
- x' = CHOOSE i \in 99 : TRUE
- Allows the value of x in the next state to be on particular number
- M \ {x}
- S \ T is the set of elements in S not in T
- e.g. (10..20) \ (1..14) = 15..20
- S \ T is the set of elements in S not in T
- Two Set constructors
- { v \in S : P}
- the subset of S consisting of all v satisfying P
- e.g. { n \in Nat : n > 17} = {18,19,20,...}
- The set of all natural numbers greater than 17
- e.g. { n \in Nat : n > 17} = {18,19,20,...}
- the subset of S consisting of all v satisfying P
- { e : v \in S }
- The set of all e for v in S
- e.g. { n^2 : n \in Nat} = {0, 1, 4, 9, ...}
- The set of all squares of natural numbers
- e.g. { n^2 : n \in Nat} = {0, 1, 4, 9, ...}
- The set of all e for v in S
- { v \in S : P}
- The LET clause makes the definitions local to the LET expressions.
- The defined identifiers can only be used in the LET expressions.
- Elements of a symmetry set, or a constant assigned elements of a symmetry set, may not appear in a CHOOSE expression.
Lesson 8
- P => Q
- if P is true, then Q is true
- the symbol ⇒ written => and is read implies
- P => Q equals ~Q => ~P
- In speech, implication asserts causality.
- In math, implication asserts only correlation.
- A module-closed expression is a TLA+ expression that contains only:
- identifiers declared locally within it
- A module-closed formula is a boolean-valued module-closed expression.
- A constant expression is a (module-complete) expression that (after expanding all definitions):
- has no declared variables
- has no non-constant operators. e.g. some non-constant operators are ' (prime) and UNCHANGED
- The value of a constant expression depends only on the values of the declared constants it contains.
- An assumptionat (ASSUME) must be a constant formula.
- A state expression can contain anything a constant expression can as well as declared variables.
- The value of a state expression depends on:
- The value of declared constants
- The value of declared variables
- A state expression has a value on a state. A state assigns values to variables.
- A constant expression is a state expression that has the same value on all states.
- An action expression can contain anything a state expression can as well as ' (prime) and UNCHANGED.
- A state expression has a value on a step (a step is a pair of states).
- A state expression is an action expression whose value on the step s -> t depends only on state s.
- An action formula is simply called an action.
- A temporal formula has a boolean value on a sequence of states (behavior)
- TLA+ has only boolean-valued temporal expressions.
- Example spec:
- Initial formula
- TPInit
- Next-state formula
- TPNext
- TPSpec should be true on s1 -> s2 -> s3 -> ... iff
- TPInit is true on s1
- TPNext is true on si -> si+1 for all i
- TPInit is considered to be an action.
- Initial formula
- ⎕ typed [] in ASCII, is read as always. The always operator.
- ⎕TPNext - "Always TPNext"
- TPSpec ≜ TPInit /\ [⎕TPNext]<<v1,v2,v3>>
- The specification with
- Initial formula Init
- Next-state formula Next
- Declared variables v1,...vn
- Is expressed by the temporal formula
- Init /\ ⎕[Next]<<v1...,vn>>
- The specification with
- For a temporal formula TF;
- THEOREM TF
- asserts that TF is true on every possible behavior.
- THEOREM TF
- THEOREM TPSpec => []TPTypeOK
- Asserts that for every behavior:
- if TPSpec is true on the bheavior
- then []TPTypeOK is true on the behavior (means TPTypeOK is true on every state of the behavior).
- Asserts that TPTypeOK is an invariant of TPSpec.
- Asserts that for every behavior:
- INSTANCE TCCommit
- THEOREM TPSpec => TCSpec
- Asserts that for every behavior:
- if it satisfies TPSpec
- then it satisfies TCSpec
- Asserts that for every behavior:
- THEOREM TPSpec => TCSpec
- Dpecifications are not programs; they're mathematical formulas.
- A specification does not describe the correct behavior of a system, rather it describes a universe in which the system and its environment are behaving correctly.
- The spec says nothing about irrelevant parts of the universe.
- THEOREM TPSpec => TCSpec
- This theorem makes sense because both formuals are assertions about the same kinds of behavior.
- It asserts that every behavior satisfying TPSpec satisfies TCSpec.
- Steps that leave all the spec's variables unchanged are called stuttering steps
- Every TLA+ spec allows stuttering steps
- We represent a terminating execution by a behavior ending in an infinite sequence of stuttering steps.
- The universe keeps going even if the system terminates.
- All behaviors are infinite sequences of states.
- Specs specify what the system may do.
- They don't specify what it must do.
- These are different kinds of requirments and should be specified seperately.
Lesson 9
- List are finite sequences.
- Tuples are simply finite sequences.
- << -3, "xyz", {0,2} >> is a sequence of length 3
- A sequence of length N is a function with domain 1..N
- << -3, "xyz", {0,2} >>[1] = -3
- << -3, "xyz", {0,2} >>[2] = "xyz"
- << -3, "xyz", {0,2} >>[3] = {0,2}
- The sequence <<1,4,9,...,N^2>> is the function such that
- <<1,4,9,...,N^2>>[i] = i^2
- for all i in 1..N
- This is writen as: [i \In 1..N |-> i^2]
- Tail(<<s1,..,sn>>) equals <<s2,...,sn>>
- Head(seq) == seq[1]
- ◦ (concatenation) written as \o concaneates two sequences
- <<3,2,1>> ◦ <<"a","b">> = <<3,2,1,"a","b">>
- Any non-empty sequence is the concaneation of it's head with it's tail
- IF seq # <<>> THEN seq = <<Head(seq)>> \o Tail(seq)
- The Append operator appends an element to the end of the sequence
- Append(seq, e) == seq \o <>
- The operator Len applied to a sequence equals the sequences' length
- Len(seq)
- The domain of a sequence seq is 1..Len(seq)
- 1..0 = {}, which is the domain of <<>>
- Seq(S) is the set of all sequences with elements in S.
- Seq({3}) = {<<>>, <<3>>, <<3,3>>, <<3,3,3>>, ...} (infinite sequences)
- Remove(i, seq) == [j \in 1..(Len(seq) - 1) |-> IF j < i THEN seq[j] ELSE seq[j + 1]]
- Len(Remove(i, seq)) = Len(seq) -1
- The Cartesian Product
- For any sets S and T
- S × T equals the set of all <<a, b>> with a ∈ S and b ∈ T
- S × T = {<<a, b>>: a \in S, b \in T}
- The × (times) operator is written as \X in ASCII.
- For any sets S and T
- A Safety Formula is a temporal formula that asserts only what may happen.
- It's a temporal formula that if a behavior violates it, then that violation occurs at some particular point in that behavior.
- Nothing past that point can prevent the violation.
- For example:
- Init /\ [][Next]vars can be violated either:
- Initial state not satisfying Init
- Step not satisfying [Next]vars
- Step neither satisfies Next nor leaves vars unchanged.
- Nothing past that point of violation can cause the formula to be true.
- Init /\ [][Next]vars can be violated either:
- For example:
- Nothing past that point can prevent the violation.
- It's a temporal formula that if a behavior violates it, then that violation occurs at some particular point in that behavior.
- A Liveness Formula is a temporal formula that asserts only what must happen.
- A temporal formula that a behavior can not violate it at any point.
- Example: x = 5 on some state of the behavior.
- asserted by (x = 5)
- ◊ is typed as <> is ASCII and is pronounced eventually
- The only liveness property sequential programs must satisfy is termination.
- Expressed by formual ◊Terminated
- is ~> is ASCII and means leads to.
- ◊P is equivalent to ¬⎕¬P
- Eventually P is equal to not always not P.
- An action A is enabled in a state s if-and-only-if there is a state t such that s → t is an A step.
- An action is enabled if the system is not in a deadlocked/terminated state. The safety part of the spec implies that such a state cannot be reached.
- A conjunct with no primes is an assertion.
- A weak fairness of action A asserts of a behavior:
- If A ever remains continiously enabled, then an A step must eventually occur.
- Or equivalenty:
- A cannot remain enabled forever without another A step occuring.
- Weak fairness of A is written as the temporal formula WF_vars(A), where vars is the tuple of all the spec's variables.
- It's a liveness property because it can always be made true by an A step or a state in which A is not enabled.
- A spec with liveness is written
- _Init /\ [][Next]vars /\ Fairness
- Fairness ia conjunction of one or more WF_vars(A) and SF_vars(A) formulas, where each A is a subaction of Next.
- A subaction of Next is when every possible A step is a Next step.
- _Init /\ [][Next]vars /\ Fairness
- WF_vars(A) asserts of a behavior:
- If A /\ (vars' # vars) ever remains continiously enabled:
- then an A /\ (vars' # vars) step must eventually occur.
- An A /\ (vars' # vars) step is a non-stuterring A step
- If A /\ (vars' # vars) ever remains continiously enabled:
- ABS == INSTANCE ABSpec
- Imports all definitions of Spec,... from ABSpec, renamed as ABS!Spec,...
- THEOREM Spec => ABS!Spec
- This theorem states that the safety specification Spec implements it's high level safety specification ABS!Spec
- Weak fairness of A asserts of a behavior:
- If A ever remains continiously enabled, then an A step must eventually occur.
- Strong fairness of action A asserts of a behavior:
- If A is repeatedly enabled, then an A step must eventually occur.
- Or equivalently:
- A cannot be repeatedly enabled forever, without another A step occuring.
- For systems without hard real-time response requirements, liveness checking is a useful way to find errors that prevent things from happening.
- Many systems use timeouts only to ensure that something must happen.
- Correctness of such a system does not depend on how long it takes the timeouts to occur.
- Specifications of these systems can describe timeouts as actions with not time constraints, only weak fairness conditions.
- This is true for most systems with no bounds on how long it can take an enabled operation to occur.
- A reason to add liveness is to catch errors in the safetey formula Spec.
Ron Pressler course notes
Part 1
- TLA+ is like a blueprint when designing a house
- In TLA+ the abstraction/implementation relation is expressed by logical implication: X ⇒ Y is the proposition that X implements Y, or conversely that Y abstracts X.
- Specifying in TLA+ is ultimately specifying with mathematics. But math doesn't save you from thinking; it just helps you organize your thoughts.
- A signature, which is a set of symbols with a specifiy arity - how many arguments the symbol takes.
- e.g. 5 (0-ary), = (2-ary), < (2-ary), * (2-ary)
- Expressions can have quantifier, like \A ("for all") and "existential quantifier" \E ("there exists")
- \A x ... means "for all objects s such that ..."
- \E x ... means "there exists an object x such that ..."
- A well-formed expression is called a term (of the language), so the syntax is thought of as the set of all the terms.
- A formula is a boolean-valued expression, either true or false.
- Variables that appear in a formula unbound are called free variables_
- A formula that has no free variables is called a sentence or closed formula
- A model is the relationship between the syntax and semantics: a model of a formula is a structure that satisfies it.
- It satisfies it by assigment of values to the variables taht make the formula true (truth is a semantic property).
- ⊨ or |= in ASCII, is the symbol for satisfies, on the left is a structure that make the formula on the right true
- The collection of all models of a formula A forms its formal semantics is written as [[A]]
- Examples
- [[A∧B]]=[[A]]∩[[B]] - the model for A /\ B is the intersection of model A with model B.
- [A∨B]]=[[A]]∪[[B]] - the model for A / B is the union of model A with model B.
- [[¬A]]=[[A]]c - the model ~A is the complement of the model A
- Ehen working with logic, we work within a specific logical theory, which is a set of formulas called axioms, taken to be equivalent to TRUE.
- A model of a theory is a structure that satisfies all axioms of the theory; the theory specifies a model.
- Peano axioms - logical theory that characterizes the natural numbers and familiar arithmetic operations
- A logic also hash a calculus a syntactic system for deriving expressions from other expressions, like natural deduction.
- If formula C can be derived by a finite number of application of inference rules from formulas A and B, we write A,B ⊢ C, and say that A and B prove C or entail C, where A and B are the assumptions.
- If formula A is entaile dby theory's axioms alone without any other assumptions, we write ⊢A and say A is a tautology
- If ⊢A and A is not an axiom, we say that A is a theorem. If we want to prove the theorem A, but we havne't yet done so, we call A a proposition
- TLC - TLA+ model checker
- TLA+ Toolbox - create specs and run tools on them
- TLAPS - the TLA+ proof system
- Deadlock - Execution stopped when it wasn't supposed to.
- Termination - Execution stopped when it was suppose to.
- The TLA+ syntax for an array valued expression:
[ variable ∈ set ↦ expression ]
- Example:
sqr ≜ [i ∈ 1..42 ↦ i^2]
- defines sqr to be an array with index set 1..42
- such that sqr[i] = i^2 for all i in 1..42
- Example:
sqr ≜ [i ∈ 1..42 ↦ i^2]
- ↦ is typed as |-> in ASCII
- In Math, we use parentheses for function application instead of brackets.
- in TLA+ we write formulas not programs so we use math terminology,
- function instead of array, domain instead of index set,
- however TLA+ uses square brackets for function application to avoid confusing with
- another way mathemiatics uses paranethesis
- Math and TLA+ allow a function to have any set as its domain, for example, the set of all integers.
- The for all symbol ∀ is typed as \A in ASCII
- the exponentiation operator is represented by the carat chractor e.g. (i^2)
- ≡ or ⇔ or <=> is "if-and-only-if" equivalence
- EXTENDS Integers - imports arithmetic operators like + and ..
- VARIABLES i, pc - Declares identifiers
- Init and Next are convention names used
- <>[]P - a termporal operator that every behaviour must conform to where eventually P becomes true and then always stays true. P may switch between true or false but must be true when program terminates.
- /\ is "AND"
- \/ is "OR"
- ~ is "not" negation
- -> is "if-then" implication
- <=> is "if-and-only-if" equivalence
- i^n is exponentiation operator
A | B |
---|---|
Programming | Math |
Array | Function |
Index Set | Domain |
f[e] | f(e) |
Compile pluscal program:
pcal program.tla
Run TLA+ program:
tlc program.tla
Generate LaTeX:
tlatex program.tla
Generate PDF from LaTeX:
pdflatex program.tex
- https://lamport.azurewebsites.net/video/videos.html
- https://lamport.azurewebsites.net/tla/summary-standalone.pdf
- https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
- https://lamport.azurewebsites.net/tla/p-manual.pdf
- https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1997-006A.pdf
- https://pron.github.io/tlaplus
- https://pron.github.io/posts/tlaplus_part1
- https://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/
- https://surfingcomplexity.blog/2014/06/04/crossing-the-river-with-tla/
- https://sookocheff.com/post/tlaplus/getting-started-with-tlaplus/
- https://www.binwang.me/2020-10-06-Understand-Liveness-and-Fairness-in-TLA.html
- https://docs.imandra.ai/imandra-docs/notebooks/a-comparison-with-tla-plus/
- https://weblog.cs.uiowa.edu/cs5620f15/PlusCal
- https://learntla.com/pluscal/a-simple-spec/
- https://jack-vanlightly.com/blog/2019/1/27/building-a-simple-distributed-system-formal-verification
- https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/overview-page.html
- https://link.springer.com/content/pdf/bbm%3A978-1-4842-3829-5%2F1.pdf
- https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.519.6413&rep=rep1&type=pdf
- https://github.com/Disalg-ICS-NJU/tlaplus-lamport-projects
- https://github.com/quux00/PlusCal-Examples
- https://github.com/sanjosh/tlaplus
- https://github.com/lostbearlabs/tiny-tlaplus-examples
- https://github.com/pmer/tla-bin
- https://github.com/hwayne/tla-snippets
- https://github.com/dgpv/SASwap_TLAplus_spec
- Lamport TLA+ Course Lectures
- Leslie Lamport: Thinking Above the Code