Skip to content

Instantly share code, notes, and snippets.

Last active September 27, 2018 14:08
What would you like to do?
PWLConf 2018 notes

Computer-aided Concurrent Programming - 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

Temporal logic primer

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)


AG q - classic safety propery EF p - classic liveness property

Reasoning about infinite computations - which is why we can say "eventually"


CTL synthesis decision procedure

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.

Abstraction-Guided Synthesis of Synchronisation - by M. Vechev, E. Yahav, and G. Yorsh (2010)

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

From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis (2016)

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

Standards We Love - Heidy Khlaaf

Bug findings

How are we not dead yet?

Verifying Nuclear Power Plants

Containment structure - reactor vessel and control rods

FPGAs Smart sensors

Companies writing their own compilers - minefield, from a verification point of view

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment