https://pwlconf.org/2018/roopsha-samanta/
Clarke and Emerson - Design and Synthesis of Sychnronization Skeletons using Branching-Time Temporal logic - Workshop on Logics of Programs (1981)
Processes are Finite-state synchronization skeletons - supress details about synchronization Communication model: Shared memory, interleaving based - one thread takes a step at a time Specification: Temporal logic Synchronization: Guarded commands Procedure: Tableau-based decision procedure
Computation-Tree Logic Model Checking for CTL CTL syntheiss
Used to reason about programs that are non-terminating ongoing systems with infinite behaviours Use Kripke structure - finite-state transition systems
Unwind into => Infinite computation tree
CTL is one way of describing these
CTL/State formula
g ::= p | !g | g_1 or g_2 | g_1 ^ g_2 | Af | Ef
Temporal operators Path quantifiers on the right (Always, Exists)
Formulas:
AG q - classic safety propery EF p - classic liveness property
Reasoning about infinite computations - which is why we can say "eventually"
EF AG q (DELTA) r
Input: CTL formula f
Is this CTL formula satisfiable?
Tableau encodes all possible models of the CTL formula - then check it for inconsistencies
It's a directed graph consisting of OR nodes and AND nodes.
ensure safety properties
Process: infinite-state program Specification: safety property Synchronization: atomic section Procedure: abstraction refinement and counterexample based (counterexample guided repair/synthesis)
Some shortcomings - it doesn't do anything to tackle the interleaving explosion problem
(It uses abstract domains to handle the state explosion problem) Someone still needs to write the assertions and know the intended behaviour of the program. Atomic sections aren't very permissive
Trace generalization-based framework to infer synchronization for an implicit Device drivers
Specification: implicit (behaviou under non-preemptive scheduler), safety property Synchronization: locks, wait-notify, etc. Procedure: counterexample generalization
More challenging verification task than the usual reachability one
trace => happens before-formula
banking example with initialization thread
- pink thread and blue thread are incrementing the account balance using their local variables safety property is that the sum must be the initial balance plus the sum of the two incrementing values
the hb formula : hb(B1,C1) ^hb(C1,B2) ^ hb(B3,A1)
Exact representation of the trace => trace generalization to a succinct hb formula - captures the essence of why it is incorrect
An atomicity violation
All incorrect related traces, no correct related traces
Automatic: HB-formula pattern => Synchronization primitive
Example: The Lock rewrite rule
Skipped the drawbacks of this paper :)
Computationally expensive
A seminal paper A modern approach A trace-based approach
CACP has come a long way, but..
- assumes sequential consistency
- simple program modesls
- simple performance models
- no optimistic concurrency control
- scalability remains a challenge
- fixed number of threads
Containment structure - reactor vessel and control rods
FPGAs Smart sensors
Companies writing their own compilers - minefield, from a verification point of view