ATVA’14 – Day 2

Below is a summary of a selection of the talks at the second day of ATVA’14.

Automatic Correctness Checking of Implementations of Concurrent Objects – Ahmed Bouajjani (Keynote)

Ahmed discusses the problem of concurrent data structures. In general, you want to implement such data structures in a library using as much concurrency as possible. However, you want to provide a simple interface to the clients that provide the ordinary, atomic operations (client view). Providing naive solutions with coarse grain locking are unacceptable; therefore, in practice, execution intervals of different library routines may overlap, yet implementations must provide this client view.

Typically, verification of librari2014-11-05 09.08.28es providing concurrent data structures is done using observation refinement. Filipovic et al. showed in 2010 that observation refinement is implied by linearizability (due to Herlihy and Wing, 1990) — Ahmed notes that this result was accepted as folklore for over a decade. The problem with using this approach is that, even when given a finite number of threads and a regular specification, checking linearizability is in EXPSPACE (Alur et al. 1996). In 2014 Had Hamza showed that it is also EXPSPACE hard. Even the simpler case of checking linearizability of a single execution is NP-complete (Gibbons and Korach, 1997), and if you have an unbounded number of threads, even with finite-state threads, linearizability is undecidable (proof is by reduction of reachability in 2-counter machines).

Given the high complexity of the observation refinement problem, Ahmed proposes a different approach. He defines a notion of history for libraries, \(H(L)\) is the history for a library \(L\). History inclusion is equivalent to observation refinement. Furthermore, \(L_1\) is linearisable w.r.t. \(L_2\) iff \(H(L_1)\) is included in \(H(L_2)\) when \(L_2\) is atomic. Not that these equivalences immediately give rise to the result that computing history inclusion is computationally hard. Therefore the idea of doing verification behind, and we focus on efficient detection of observation refinement violations to find bugs. This can be done using an under-approximation schema.

Histories can be weakened in the sense that \(h_1\) is weaker than \(h_2\) (\(h_1 \leq h_2\)) iff \(h_1\) has less constraints than \(h_2\). If \(h_1 \leq h_2\) and \(h_2\) is in \(H(L)\) for library \(L\) then \(h_1\) is in \(H(L)\) too (on a high-level, we do ignore some details here). Now you can define an approximation \(A_k(h)\), such that \(A_k(h) \leq h\) for all \(k\), an for some \(k\) it is the case that \(h \leq A_k(h)\) (i.e. there is an approximation that returns the original history. Now, suppose that we have a history \(h\) such that \(A_k(h)\) in \(H(L_1)\) (so \(h\) in \(H(L_1)\)), and \(A_k(h)\) is not in \(H(L_2)\). Then we know that \(h\) is not in \(H(L_2)\), and we have found a counter example with respect to history inclusion using the abstraction, thus we discovered a bug. The abstraction (bounding) concept is based on the notion of interval-length, and ultimately checking is done using counting. For details I refer you to Ahmed’s slides.

The Context-Freeness Problem is coNP Complete for Flat Counter Systems – Vincent Penelle

Model: state machine with positive counters; edges have guards and updates over counters. Context-freeness proof is done in a number of steps. First semi-linear sets are considered (union of linear sets) A semi-linear set is stratifiable iff it is the union of linear sets with a stratified set of periods. A theorem by Ginsburg, 1966, relates context freeness of languages to stratifiable semilinear sets. For a subclass of semilinear sets, integral polyhedra, the stratifiability problem is coNP complete.

In flat counter systems, constraints can be expressed as integral polyhedra, so, the question whether the language of S is context-free is equivalent to the question whether the corresponding integer polyhedron is stratifiable.

Flat counter systems are interesting as an object of study for complexity reasons. There is a parallel with VAS systems, where flat VAS are used as a skeleton to solve the complexity for the general case.

Deciding Entailments in Inductive Separation Logic with Tree Automata – Tomas Vojnar (fix name)

Separation logic is used for reasoning about heaps. Unbounded heaps are described using systems of inductive definitions. A nice example of an inductive definition is that of the doubly linked list using the \(DLL(h,p,t,n) = …\) predicate. The inductive definitions the approach allows have some restrictions, yet it is shown how these restrictions can be lifted (sometimes leading to incompleteness, however).

The approach proposed is to reduce entailment \(\varphi \models \psi\) to checking \(L(A_{\varphi}) \subseteq L(A_{\psi})\), where \(A_{\varphi}\) and \(A_{\psi}\) are tree automata recognising unfolding trees of the inductive definitions \(\varphi, \psi\). The tree automata are deterministic, and the construction is based on tiles such that every predicate \(P\) is represented by a single tile, and a single tile maps to a single TA state \(q_P\). Soundness follows directly from the construction. For completeness canonisation and rotation closure is used. The described approach is EXPTIME complete.

 

A Mechanised Proof of Loop Freedom of the (untimed) AODV routing protocol – Peter Hoefner and Rob van Glabbeek

In this talk, Peter and Rob consider the correctness of a routing protocol in wireless mesh networks (WMNs). In practice WMNs are unreliable and have poor performance. One of the causes for this could be the underlying routing protocols. As an example, they study an ad hoc on-demand distance vector protocol. On a high level, the protocol works as follows: if route is needed route request is broadcast; if a node receives such a request, and has no information it forwards the request; if a node has information about a destination a route reply is sent back in unicast; if unicast fails or a link break is detected a route error is sent using a group cast message. The description of the protocol relies on a routing table.

Properties that are relevant for the correctness of such a protocol are: route correctness, loop freedom, route discovery, packet delivery. In the verification they describe here, they consider loop freedom: you do not keep sending around packets indefinitely. The verification is performed using the following steps:

  • Formal specification made in the process algebra AWN (process algebra suited for specifying routing protocols). AWN extends process algebras with data structures, network-specific primitives such as (local) broadcast and (conditional) unicast, and it has a layered structure, allowing processes, nodes, networks of nodes and encapsulation. The specification consists of 6 processes, totalling about 150 lines of specification (the original standard is 40 pages of English prose).
  • Pen-and-paper proof of loop freedom: 20 pages, using 40 invariants (state/transition invariants talking about one or more nodes).
  • Mechanized proof: formalised Isabelle/HOL. One part is mechanization of process algebra AWN (ITP’14). Mechanization of the loop-freedom proof consists of 360 lemmas of which 40 are invariants, with the usual mechanisation overhead.
    • Node properties are often straightforward to prove.
    • Network properties are harder because the describe relations between multiple nodes; stating the properties alone in a machine readable way is already hard.

The total effort of doing the mechanised verification is estimated to be 1 person-year, of which about 8 months were devoted to the formalisation of AWN, and about 4 months were for the verification of the routing protocol.

One of the most interesting parts of the talk is the reflection on the mechanisation process (or, did they waste their time?) Here they observe that, when verifying variants of the protocol — that appear naturally due to different interpretations of the natural language standard — a lot of time can be saved. They illustrate this observation by reporting on variants they verified: in 5 variations in which the lemmas and invariants that were formulated were preserved, the formalisation and proofs could be fixed very easily (in a matter of hours). You are not always lucky, though, since if the lemmas do not hold in their original form any longer, you will need more expertise to fix the proofs, and the fixing is not so straightforward as in the other cases.

 

Using Flow Specifications of Parameterised Cache Coherence Protocols for Verifying Deadlock Freedom – Sharad Malik

Cache coherence protocols gives shared memory view to multiple processors with individual caches and main memory. A well-known example of a cache coherence protocol is that for guaranteeing exclusive access in the German protocol. In this case, concurrent requests may lead to contention, and eventually to deadlock (where system-wide deadlock, or s-deadlock is considered).

Given a protocol P(N) with N an unbounded number of caches, the problem addressed is to verify freedom of s-deadlock on it. Prior work in this area mainly applies to mutual exclusion (no two caches have exclusive access at the same time); in that case, counterexamples typically involve just two caches because the property has a two-index property. For deadlock freedom, all caches are involved, hence counter examples might involve all caches. This makes that approaches that work in the mutual exclusion setting do not generally carry over to the setting of checking absence of s-deadlock.

Sharad describes a nice approach to verifying s-deadlock, which is based on the following idea. Establish a set of invariants that are stronger than s-deadlock, that do allow for verification using existing approaches. Once such invariants are established s-deadlock immediately follows. In order to establish such invariants, he uses flows (these are high-level descriptions of protocols). The invariants that are determined are such that some flow is enabled at all times, immediately implying absence of s-deadlock.

To determine such invariants, a looping process is started, where initially a number of straightforward invariants is given (that do not necessarily hold). These invariants are verified using model checking on a small number of agents. If the invariants hold for this small number of agents, then they proceed to verifying that they also hold for arbitrary N. If the invariants do not hold, the user is asked to refine the invariants, and the process repeats.

One of the open questions, and in my opinion a very important one, is whether invariants can automatically be refined when they fail during the model checking phase.