Static Verification of Concurrent Programs using Reduction and Abstraction

Add to your list(s) Download to your calendar using vCal

• Tayfun Elmas - Koc University, Istanbul
• Thursday 29 April 2010, 14:00-15:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: Concurrency-related bugs are notoriously difficult to discover by code review and testing. By doing a formal proof on the program text, one can statically verify that no execution of the program leads to an error. The effectiveness of the proof depends on the proper choice of the manual inputs such as code annotations. Deriving these annotations for a concurrent program requires complicated reasoning. The main reason behind this is the interaction between threads over the shared memory. While writing the proof, at every point, one has to consider the possible interleavings of conflicting operations. Existing proof methods including Owicki-Gries, rely/guarantee and concurrent separation logic are applied at the finest level of concurrency. Analyzing the program at this level requires complex annotations and invariants, along with many auxiliary variables.

In this talk, we present a new proof method that simplifies verifying assertions and linearizability in concurrent programs. The key feature of our method is the use of atomicity as the main proof tool. A proof is done by rewriting the program with larger atomic blocks in a number of steps. In order to reach the desired level of atomicity, we alternate proof steps that apply abstraction and reduction, each of which improves the outcome of the other in a following step. Then, we check assertions sequentially within the atomic blocks of the resulting program. We declare the original program correct when we discharge all the assertions. Our proof style provides separation of concerns: At each step, we either use facts about a concurrency protocol to enlarge atomic blocks, or check data properties sequentially. Our software tool, QED , mechanizes proofs using the Z3 SMT solver to check preconditions of the proof steps. We demonstrated the simplicity of our proof strategy by verifying well-known programs using fine-grained locking and non-blocking data algorithms.

Biography:* Tayfun Elmas is a Ph.D. candidate at Koc University (Istanbul, Turkey), advised by Dr. Serdar Tasiran (Koc Univ.) and Dr. Shaz Qadeer (Microsoft Research). His research interests are formal methods and tools for the debugging, analysis, and verification of concurrent software. Tayfun`s recent work appeared at premier programming languages conferences (PLDI, POPL , TACAS), workshops (RV, FATES , PADTAD), and national conferences (UYMS, YKGS ). His research is supported by the Scientific and Technological Research Council of Turkey (TUBITAK), the Turkish Academy of Sciences (TUBA) and Microsoft Research. The Goldilocks project he primarily involved has been selected for publication in SIGPLAN CACM Research Highlights. Tayfun was an intern at Microsoft Research (Redmond,WA) during the summer of 2005 and 2007. He received his B.S. in Computer Engineering from Ege University (Izmir, Turkey) in 2003, and M.S. in Electrical and Computer Engineering from Koc University in 2005.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.