TY - CONF
AB - Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.
AU - Cerny, Pavol
AU - Radhakrishna, Arjun
AU - Zufferey, Damien
AU - Chaudhuri, Swarat
AU - Alur, Rajeev
ID - 4390
TI - Model checking of linearizability of concurrent list implementations
VL - 6174
ER -
TY - CONF
AB - Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.
AU - Cerny, Pavol
AU - Henzinger, Thomas A
AU - Radhakrishna, Arjun
ID - 4393
TI - Simulation distances
VL - 6269
ER -
TY - CONF
AB - Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.
AU - Beyer, Dirk
AU - Henzinger, Thomas A
AU - Théoduloz, Grégory
AU - Zufferey, Damien
ED - Rosenblum, David
ED - Taenzer, Gabriele
ID - 4396
TI - Shape refinement through explicit heap analysis
VL - 6013
ER -
TY - CONF
AB - Efficient zero-knowledge proofs of knowledge (ZK-PoK) are basic
building blocks of many practical cryptographic applications such as
identification schemes, group signatures, and secure multi-party
computation (SMPC). Currently, first applications that essentially
rely on ZK-PoKs are being deployed in the real world. The most
prominent example is the Direct Anonymous Attestation (DAA)
protocol, which was adopted by the Trusted Computing Group (TCG)
and implemented as one of the functionalities of the cryptographic
chip Trusted Platform Module (TPM).
Implementing systems using ZK-PoK turns out to be challenging,
since ZK-PoK are significantly more complex than standard crypto
primitives (e.g., encryption and signature schemes). As a result,
the design-implementation cycles of ZK-PoK are time-consuming
and error-prone.
To overcome this, we present a compiler with corresponding languages
for the automatic generation of sound and efficient ZK-PoK based on
Σ-protocols. The protocol designer using our compiler formulates
the goal of a ZK-PoK proof in a high-level protocol specification language,
which abstracts away unnecessary technicalities from the designer. The
compiler then automatically generates the protocol implementation in
Java code; alternatively, the compiler can output a description of the
protocol in LaTeX which can be used for documentation or verification.
AU - Bangerter, Endre
AU - Briner, Thomas
AU - Henecka, Wilko
AU - Stephan Krenn
AU - Sadeghi, Ahmad-Reza
AU - Schneider, Thomas
ED - Martinelli, Fabio
ED - Preneel, Bart
ID - 2980
TI - Automatic Generation of Sigma-Protocols
VL - 6391
ER -
TY - JOUR
AB - Development of plants and their adaptive capacity towards ever‐changing environmental conditions largely depend on the spatial distribution of the plant hormone auxin. At the cellular level, various internal and external signals are translated into specific changes in the polar, subcellular localization of auxin transporters from the PIN family thereby directing and redirecting the intercellular fluxes of auxin. The current model of polar targeting of PIN proteins towards different plasma membrane domains encompasses apolar secretion of newly synthesized PINs followed by endocytosis and recycling back to the plasma membrane in a polarized manner. In this review, we follow the subcellular march of the PINs and highlight the cellular and molecular mechanisms behind polar foraging and subcellular trafficking pathways. Also, the entry points for different signals and regulations including by auxin itself will be discussed within the context of morphological and developmental consequences of polar targeting and subcellular trafficking.
AU - Grunewald, Wim
AU - Friml, Jirí
ID - 3072
IS - 16
JF - EMBO Journal
TI - The march of the PINs: Developmental plasticity by dynamic polar targeting in plant cells
VL - 29
ER -