ewd998 icon indicating copy to clipboard operation
ewd998 copied to clipboard

Published 20 hours ago • verified publisher icon tlaplus-workshops

Workshop Agenda

Open lemmy opened this issue 2 years ago • 0 comments

Part A

  1. Basics
  2. Actions
  3. Invariants
  4. Implication
  5. Implied Init & Box/Always
  6. [A]_v
  7. Temporal Formual: Spec
  8. ENABLED
  9. <<A>>_v
  10. Diamond/Eventually (liveness)
  11. Stuttering
  12. <>[] and []<>
  13. Fairness
  14. Weak Fairness
  15. Leads-to

Basics ..v02b09

  • CONSTANT, VARIABLES, definitions
  • set-theory refresher
  • Initial predicates and actions
  • Functions (arrays), boolean connectives (lists), unchanged and prime
  • Predicate logic/FOL - Quantification and non-determinism
  • deadlocks, state-space explosion, and small-model hypothesis
  • Specs vs. model-checking (MCInit)

TLA

First invariant TypeOK ..v02b10

  • Find bug in Wakeup action: @-2
  • Variable terminationDetected , priming operators

Property Stable (Implication, Implied Inits and Box) ..v02b13

  • Introduce Implication
  • P: Rewrite terminated to FALSE and check with TLC to show vacuously true formulas (pitfall)
  • P: Revert to original terminated and show that it holds
  • V: Add FALSE to MCInit and show that it doesn't actually hold because the current formula is just an Implied Init
  • Verification doesn't find the bug unless the faulty state is an initial state
  • This is why we need the box operator to say that Stable holds in every state of a behavior; not just the initial states

Property Stable (Box to Box Box) ..v02b18

  • V: [](t => td)
    • violated by a behavior of two states (this is an invariant and checked as such)
  • V: [](t => []td)
    • we strengthen Stable to turn the invariant into a property to show that TLC checks it differently and hint at "stuttering"
  • Have we found flaw?
  • P: [](td => []t
    • No, reverse td and t , which is what we actually meant

Be suspicious of success aka non-properties, and Spec ..v02b20

  • Run simulation mode to find bogus action constraint (Always be suspicious of success)
  • Property OnlyTerminates (subscript of [N]_v <=> N \/ v'=v)
    • Every step is a Termiation step
  • These commits bridge to Spec by adding the disjunct of all actions
  • Once we arrive at Init /\ [][Next]_vars, we will revisit the implied inits and why it is useful

ENABLED ..v02b30

  • P: []ENABLED Next
    • because DetectTermination is permanently enabled and allows vars to remain unchanged)
  • V: []ENABLED Next
    • Violation after enablement of DetectTermination is changed
  • P: []ENABLED [Next]_v
    • This is a tautology
  • V: []ENABLED <<Next>>_vars
    • Violated even with UNCHANGED vars because vars don't change anymore which is stipulated by "Angle A sub variables"
    • This property is violated even with the original definition of DetectTermination that allowed infinite stuttering.

Diamond operator <>, fairness, and machine closure (prophecy) ..v02b35

  • V: <>terminationDetected and <>terminated
    • both violated because of lack of fairness
    • Talk about comibining <> and [] into []<> and <>[] to grok (weak fairness below)
  • P: F == <>t /\ <>td
    • Turn both properties into fairness properties (not machine closed)
  • V: <>[](ENABLED <<Next>>_vars) => []<><<Next>>_vars
    • because fairness is on Next causing a lasso between Send and Wakeup
  • V: WF_vars(Next)
    • just syntactic sugar for previous property. The liveness properties are too strong, because we want to allow infinite computations, no?

Leads-to ..v02b37

  • P: [](terminated => <>terminationDetected
  • P: terminated ~> terminationDetected
    • just syntactic sugar

Inductive invariant ..v02e03

  • Validate TypeOK with Apalache
  • Prove TypeOK
  • Validate Stable with Apalache
  • Prove Stable

Part B

Simulate real modeling

Records ..v03a08

IF-THEN-ELSE ..v03a10

CHOOSE ..v03a14

Refinement ..v03b10

CHOOSE again! ..v03c04

  • Meet the TLA+ debugger

Safra's inductive invariant ..03d02

Recursion functions vs. operators and folds (community modules) ..v03d05

Part C

Validating inductive invariants (again) ..v03d07

Sketch a real Prove ..v03d08

Proof of refinement of ATD => STD (which is implemented by EWD480) ..v03e01

  • Refinement proof EWD998 => AsyncTerminationDetection (inspired by https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840_proof.tla)

Part D

Multiple nodes terminate simultaneously ..v04a02

Part E

Shiviz/ICG (trace expressions)

Channels

  • Singleton
  • refinement can
    • deconstruct variables (token changed from a (record) variable to a message kept in an inbox variable)
    • drop state (payload messages)
  • Seq in [Node -> Seq(Message)]

Executing spec with PlusPy & TLC

  • TLABlockingQueue
  • QSort
  • https://github.com/tlaplus/CommunityModules/issues/41
  • https://github.com/lemmy/AsyncGameOfLife
  • https://github.com/tlaplus/Examples/tree/mku-ewd998/specifications/ewd998
  • https://github.com/tlaplus/Examples/commits/mku-ewd998

TLA+ statistics with EWD840

  • https://github.com/tlaplus/tlaplus/issues/601
  • https://github.com/lemmy/ewd840/blob/mku-simulate-new/README.md#results

Animations

https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998_anim.tla

lemmy avatar Sep 24 '21 21:09 lemmy