{{ message }}

Instantly share code, notes, and snippets.

# msgodf/pwlconf2018.md

Last active Sep 27, 2018
PWLConf 2018 notes

# Computer-aided Concurrent Programming - Roopsha Samanta

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

### 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)

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

### 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

• 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

# Standards We Love - Heidy Khlaaf

## 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