********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--16h00 * * Salle W (Toits du DI) * * ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 14 janvier 2011, 14h00-15h00 ************************* Automatic program analysis of overlaid data structures Oukseh Lee, Hanyang University (Korea) and Queen Mary University (London) Re'sume'/ Abstract: We call a data structure overlaid, if a node in the structure includes links for multiple data structures and these links are intended to be used at the same time. These overlaid data structures are frequently used in systems code, when implementing multiple types of indexing structures over the same set of nodes. For instance, the deadline IO scheduler of Linux has a queue whose node has links for a doubly-linked list as well as those for a red-black tree. The doubly-linked list here is used to record the order that nodes are inserted in the queue, and the red-black tree provides an efficient indexing structure on the sector fields of the nodes. In this talk, I will describe an automatic program analysis of these overlaid data structures. The focus of the talk will be on two main issues: to represent such data structures effectively and to build an efficient yet precise program analyser, which can prove the memory safety of realistic examples, such as the Linux deadline IO scheduler. During the talk, I will explain how we addressed the first issue by the combination of standard classical conjunction and separating conjunction from separation logic. Also, I will describe how we used a meta-analysis and the dynamic insertion of ghost instructions in solving the second issue. If time permits, I will give a demo of the tool. This is a joint work with Oukseh Lee and Rasmus Petersen. *** Vendredi 14 janvier 2011, 15h00-16h00 ************************* Verifying Linearizability with Hindsight Noam Rinetzky, Queen Mary University (London) Re'sume'/ Abstract: Verifying concurrent algorithms that manipulate unbounded pointer-linked data structures is a challenging problem because it involves reasoning about spatial and temporal interaction between concurrently running threads. We suggest a novel approach for verification of concurrent algorithms which separates the reasoning about the algorithmic insight from the verification of its implementation. In this talk, we exemplify our approach by presenting a proof of safety, linearizability, and progress of a highly concurrent optimistic set algorithm. The key step in our proof is the Hindsight Lemma, which allows a thread to infer the existence of a global state in which its operation can be linearized based on limited local atomic observations about the shared state. The Hindsight Lemma allows us to avoid one of the most complex and non-intuitive steps in reasoning about highly concurrent linearizable algorithms: considering the linearization point of an operation to be in a different thread than the one executing it. The Hindsight Lemma assumes that the algorithm maintains certain simple invariants which are resilient to interference, and which can themselves be verified using purely thread-local proofs. As a consequence, the lemma allows us to unlock a perhaps-surprising intuition: a high degree of interference makes non-trivial highly concurrent algorithms in some cases much easier to verify than less concurrent ones. Joint work with Peter O'Hearn, Martin Vechev, Eran Yahav and Greta Yorsh, published in PODC'10. ********************************************************************* Pour recevoir l'annonce par courrier electronique: WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************