Repository files navigation

Some examples and notes while learningTLA+ 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 calledabstraction
• 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:
  1. All possible initial states.
  2. 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.
  1. Possible initial values of variables.
  2. A relation between their values in the current state and their possiblevalues in the next state.

Lesson 2

• We need precise language to describe state machines
• TLA+ uses ordinary, simple math
• Must replaceAND (&&) by a mathimatical operator∧ (logical AND)
• Must replaceOR (||) by a mathimatical operator∨ (logical OR)
• "i in {0,1,...,1000} is written asi ∈ 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 in2 + 2 = 4unlike 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≜ meansequal 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 aninvariant
• The not equal operator is≠ and is written in ASCII as/= or#
• ≤ is=< in TLA+ ASCII
• To keep things simple, use a primed variablev' only in one of these two kinds of formulas:
  • v' = ... andv' ∈ ... where... contains no primed variables
• comment out blocks with(* and*)
• ∃ meansThere is exists and is writen as\E in ASCII.

Lesson 5

• UseCONSTANT 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]
      • definesr to be a record with two fieldsprof andnum.
      • The values of it's two fields are
        • r.prof = "Fred" andr.num = 42
    • Chaning the order of the fields makes no difference
  • TLA+ format is
    • [prof : {"Fred", "Ted", "Ned"}, num : 0..99]
      • is the set of all records
        • [prof |-> ..., num |-> ...]
      • withprof field in set{"Fred", "Ted", "Ned"} and
        • num field in set0..99
    • So[prof |-> "Ned", num |-> 24] is in this set.
  • This record is a function
    • [prof |-> "Fred", num |-> 42]
      • is a functionf with domain{"prof", "num"}
      • such thatf["prof"] = "Fred" andf["num"] = 42
  • f.prof is an abbreviation forf["prof"]
  • This except expression equals the record that is the same asf except it'sprof field is the string red
    • [f EXCEPT !["prof"] = "Red"]
      • this can be abbreviated as
        • [f EXCEPT !.prof = "Red"]
• Subset⊆ is written as\subseteq in ASCII and readis a subset of
• Union set operator∪ is written as\union in ASCIIS ∪ T is the set of all elementsS orT 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 av inS for whichP is true
    • then some suchv
    • else a completely unspecified value
• 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 ofx in the next state to be any number in1..99
• x' = CHOOSE i \in 99 : TRUE
  • Allows the value ofx in the next state to be on particular number
• M \ {x}
  • S \ T is the set of elements inS not inT
    • e.g.(10..20) \ (1..14) = 15..20
• Two Set constructors
  • { v \in S : P}
    • the subset ofS consisting of allv satisfyingP
      • e.g.{ n \in Nat : n > 17} = {18,19,20,...}
        • The set of all natural numbers greater than17
  • { e : v \in S }
    • The set of alle forv inS
      • e.g.{ n^2 : n \in Nat} = {0, 1, 4, 9, ...}
        • The set of all squares of natural numbers
• TheLET clause makes the definitions local to theLET expressions.
  • The defined identifiers can only be used in theLET expressions.
• Elements of a symmetry set, or a constant assigned elements of a symmetry set, may not appear in aCHOOSE expression.

Lesson 8

• P => Q
  • ifP is true, thenQ is true
  • the symbol⇒ written=> and is readimplies
• P => Q equals~Q => ~P
• In speech, implication assertscausality.
• In math, implication asserts onlycorrelation.
• Amodule-closed expression is a TLA+ expression that contains only:
  • identifiers declared locally within it
• A module-closedformula 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) andUNCHANGED
• 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) andUNCHANGED.
• 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 steps -> t depends only on states.
• 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 ons1 -> s2 -> s3 -> ... iff
  • TPInit is true ons1
  • TPNext is true on s_i -> s_i+1 for alli
  • TPInit is considered to be an action.
• ⎕ typed[] in ASCII, is read asalways. Thealways operator.
• ⎕TPNext - "Always TPNext"
• TPSpec ≜ TPInit /\ [⎕TPNext]<<v1,v2,v3>>
  • The specification with
    • Initial formulaInit
    • Next-state formulaNext
    • Declared variablesv1,...vn
  • Is expressed by the temporal formula
    • Init /\ ⎕[Next]<<v1...,vn>>
• For a temporal formula TF;
  • THEOREM TF
    • asserts thatTF is true on every possible behavior.
• THEOREM TPSpec => []TPTypeOK
  • Asserts that for every behavior:
    • ifTPSpec is true on the bheavior
    • then[]TPTypeOK is true on the behavior (meansTPTypeOK is true on every state of the behavior).
  • Asserts thatTPTypeOK is an invariant ofTPSpec.
• INSTANCE TCCommit
  • THEOREM TPSpec => TCSpec
    • Asserts that for every behavior:
      • if it satisfiesTPSpec
      • then it satisfiesTCSpec
• 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 arebehaving 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 satisfyingTPSpec satisfiesTCSpec.
• 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 systemmay do.
  • They don't specify what itmust 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 length3
• A sequence of lengthN is a function with domain1..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 alli in1..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)
• TheAppend operator appends an element to the end of the sequence
  • Append(seq, e) == seq \o <>
• The operatorLen applied to a sequence equals the sequences' length
  • Len(seq)
• The domain of a sequenceseq is1..Len(seq)
  • 1..0 = {}, which is the domain of <<>>
• Seq(S) is the set of all sequences with elements inS.
  • 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 setsS andT
    • S × T equals the set of all<<a, b>> witha ∈ S andb ∈ T
    • S × T = {<<a, b>>: a \in S, b \in T}
  • The× (times) operator is written as\X in ASCII.
• ASafety Formula is a temporal formula that asserts only whatmay 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 satisfyingInit
          • Step not satisfying[Next]vars
            • Step neither satisfiesNext nor leavesvars unchanged.
        • Nothing past that point of violation can cause the formula to be true.
• ALiveness Formula is a temporal formula that asserts only whatmust happen.
  • A temporal formula that a behavior cannot 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 pronouncedeventually
• The only liveness property sequential programs must satisfy istermination.
  • Expressed by formual◊Terminated
• is~> is ASCII and meansleads to.
• ◊P is equivalent to¬⎕¬P
  • EventuallyP is equal tonot always not P.
• An actionA isenabled in a states if-and-only-if there is a statet such thats → t is anA 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 actionA asserts of a behavior:
  • IfA ever remains continiously enabled, then anA step must eventually occur.
  • Or equivalenty:
    • A cannot remain enabled forever without anotherA step occuring.
• Weak fairness ofA is written as the temporal formulaWF_vars(A), wherevars is the tuple of all the spec's variables.
  • It's aliveness property because it can always be madetrue by anA step or a state in whichA is not enabled.
• A spec with liveness is written
  • _Init /\ [][Next]vars /\ Fairness
    • Fairness ia conjunction of one or moreWF_vars(A) andSF_vars(A) formulas,where eachA is a subaction ofNext.
  • A subaction ofNext is when every possibleA step is aNext step.
• WF_vars(A) asserts of a behavior:
  • IfA /\ (vars' # vars) ever remains continiously enabled:
    • then anA /\ (vars' # vars) step must eventually occur.
  • AnA /\ (vars' # vars) step is a non-stuterringA step
• ABS == INSTANCE ABSpec
  • Imports all definitions ofSpec,... fromABSpec,renamed asABS!Spec,...
• THEOREM Spec => ABS!Spec
  • This theorem states that the safety specificationSpec implements it's high level safety specificationABS!Spec
• Weak fairness ofA asserts of a behavior:
  • IfA ever remains continiously enabled, then anA step must eventually occur.
• Strong fairness of actionA asserts of a behavior:
  • IfA is repeatedly enabled, then anA step must eventually occur.
  • Or equivalently:
    • A cannot be repeatedly enabled forever, without anotherA 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 formulaSpec.

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 thatX implementsY, or conversely thatY abstractsX.
• 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 specifiyarity - how many arguments the symbol takes.
  • e.g.5 (0-ary),= (2-ary),< (2-ary),* (2-ary)
• Expressions can havequantifier, 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 aterm (of the language), so the syntax is thought of as the set of all the terms.
• Aformula is a boolean-valued expression, eithertrue orfalse.
• Variables that appear in a formula unbound are calledfree variables_
• A formula that has no free variables is called asentence orclosed formula
• Amodel is the relationship between the syntax and semantics: a model of a formula is a structure thatsatisfies 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 forsatisfies, on the left is a structure that make the formula on the right true
• The collection of all models of a formula A forms itsformal semantics is written as[[A]]
• Examples
  • [[A∧B]]=[[A]]∩[[B]] - the model forA /\ B is the intersection of model A with model B.
  • [A∨B]]=[[A]]∪[[B]] - the model forA / 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 specificlogical theory, which is a set of formulas calledaxioms, 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 acalculus a syntactic system for deriving expressions from other expressions, likenatural deduction.
  • If formulaC can be derived by a finite number of application of inference rules from formulasA andB, we writeA,B ⊢ C, andsay that A and Bprove C orentail C, where A and B are the assumptions.
  • If formulaA is entaile dby theory's axioms alone without any other assumptions, we write⊢A and sayA is atautology
  • If⊢A andA is not an axiom, we say thatA is atheorem. If we want to prove the theoremA, but we havne't yet done so, we callA aproposition

• 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]
    • definessqr to be an array with index set1..42
    • such thatsqr[i] = i^2 for all i in 1..42
• ↦ 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 andNext 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

Compile pluscal program:

pcal program.tla

Run TLA+ program:

tlc program.tla

Generate LaTeX:

tlatex program.tla

Generate PDF from LaTeX:

pdflatex program.tex

• http://lamport.azurewebsites.net/video/videos.html
• https://lamport.azurewebsites.net/tla/summary-standalone.pdf
• http://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

MIT