(EC)2 2016: 9th International Workshop on Exploiting Concurrency Efficiently and Correctly
July 18, 2016
|9:00 - 9:45||
(Microsoft Research), |
Refinement: an essential technique for reasoning about concurrency
|9:45 - 10:30||
(MIT CSAIL), |
On Language Support for Fault-tolerance in Distributed Systems
|10:30 - 11:00||Morning break|
|11:00 - 11:45||
(University of Utah), |
"Formal Methods for High-Performance Computing: Finding Data Races in Large OpenMP Applications"
|11:45 - 12:30||
(Academia Sinica, Taiwan), |
"The Commutative Problem of MapReduce programs"
|12:30 - 14:00||Lunch break|
|14:00 - 14:45||
(Paris 7), |
"Linearizability Checking: Reductions to State Reachability"
|14:45 - 15:30||
(Princeton University), |
"Incremental Proofs for Parameterized Programs"
|15:30 - 16:00||Afternoon break|
|16:00 - 16:45||
(USTC, China), |
"Reasoning about progress of concurrent objects"
We are very excited to have the following confirmed invited speakers for the workshop:
Shaz Qadeer, Microsoft Research
Refinement: an essential technique for reasoning about concurrency
The refinement approach to program correctness considers abstract programs as specifications of concrete programs. In this talk, I will argue that refinement is essential for reasoning about concurrent programs. I will draw upon my experience building two verification-oriented concurrent programming systems. First, I will discuss the P/P# family of domain-specific languages that provide systematic testing capability to asynchronous actor programs; P and P# have been used for designing, implementing, and testing device drivers and distributed services in a variety of Microsoft product groups. Second, I will discuss CIVL, a verifier for fine-grained shared-memory programs; CIVL has been used for implementing a realistic concurrent garbage collector using only atomic load and store primitives. I will demonstrate that despite the difference in analysis techniques, testing in the former and inductive proofs in the latter, refinement is a tremendous aid in both approaches. My experience provides evidence for the conclusion: program reasoning systems that aim to combine testing and verification must attempt to incorporate refinement.
Biography: Shaz Qadeer is a Principal Researcher at Microsoft. He is a member of the Research in Software Engineering group at Microsoft Research. His work aims to improve software reliability by providing programmers with automated tools to analyze their programs. Most of his work has focused on analysis of concurrent software.
Damien Zufferey, MIT CSAIL
On Language Support for Fault-tolerance in Distributed Systems
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. First, I review some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system and present different models that have been proposed to reason about distributed algorithms. Then I introduce PSync a domain specific language which views asynchronous systems as synchronous ones with an adversarial environment that drops or delays messages. Even though PSync programs look synchronous, they execute efficiently over asynchronous networks. The advantage of PSync is twofold: the synchronous abstraction simplifies the design and implementation of fault-tolerant distributed algorithms and enables semi-automated formal verification.
This is joint work with Cezara Dragoi, Thomas A. Henzinger, Josef Widder, and Helmut Veith.
Biography: Damien Zufferey is a Postdoctoral researcher in Martin Rinard's group at MIT CSAIL since Octorber 2013. Before moving to MIT, He obtained a PhD at the Institute of Science and Technology Austria (IST Austria) under supervision of Thomas A. Henzinger in September 2013 and a Master in computer science from EPFL in 2009. He is interested in improving software reliability by developing theoretical models, building analysis tools, and giving the programmer the appropriate language constructs. He is particularly interested in the study of complex concurrent systems. His research lies at the intersection of formal methods and programming languages.
Zvonimir Rakamaric, University of Utah
Formal Methods for High-Performance Computing: Finding Data Races in Large OpenMP Applications
OpenMP plays a central role as a portable programming model to harness on-node parallelism in high-performance computing applications; yet, existing data race checkers for OpenMP have high overheads and generate many false positives. In this talk, I will describe our OpenMP data race checker called Archer, that achieves high accuracy, low overheads on large applications, and portability. Archer incorporates scalable happens-before tracking, exploits structured parallelism via combined static and dynamic analysis, and modularly interfaces with OpenMP runtimes. Our empirical evaluation shows that it significantly outperforms related tools, while providing the same or better precision. It has helped detect critical data races in the Hypre library that is central to many projects at Lawrence Livermore National Laboratory and elsewhere.
Biography: Zvonimir Rakamaric is an assistant professor in the School of Computing at the University of Utah. Prior to this, he was a postdoctoral fellow at Carnegie Mellon University in Silicon Valley, where he worked closely with researchers from the Robust Software Engineering Group at NASA Ames Research Center to improve the coverage of testing of NASA's flight critical systems. Zvonimir received his bachelor's degree in Computer Science from the University of Zagreb, Croatia; he obtained his M.Sc. and Ph.D. from the Department of Computer Science at the University of British Columbia, Canada.
Zvonimir's research mission is to improve the reliability and resilience of complex software systems by empowering developers with practical tools and techniques for analysis of their artifacts. He is a recipient of the NSF CAREER Award, Microsoft Research Software Engineering Innovation Foundation (SEIF) Award 2012, Microsoft Research Graduate Fellowship 2008-2010, Silver Medal in the ACM Student Research Competition at the 32nd International Conference on Software Engineering (ICSE) 2010, and the Outstanding Student Paper Award at the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.
Yu-Fang Chen, Academia Sinica, Taiwan
The Commutative Problem of MapReduce programs
MapReduce is a popular programming model for data-parallel computation. In MapReduce, the reducer produces an output from a list of inputs. Due to the scheduling policy of the platform, the inputs may arrive at the reducers in a different order. The commutativity problem of reducers asks if the output of a reducer is independent of the order of its inputs.
Although the problem is undecidable in general, the MapReduce programs in practice are usually used for data analytics and thus require very simple data and control flow, which shed light on solving some practical instances of the problem. Today I will talk about our current progress towards a complete solution to the commutative problem.
Biography: Yu-Fang Chen is an associate research fellow at the Institute of Information Science, Academia Sinica, Taiwan. He was an assistant research fellow at the same institute from 2009 to 2014. He finished his Ph.D. study at the National Taiwan University in 2008 and wrote his doctoral thesis on the topic of the automation of compositional verification using automata learning algorithms. In 2009, he worked as a postdoc researcher at Uppsala University, Sweden.
His current research focus includes (1) applications of formal methods in MapReduce programs and (2) synthesis and analysis models of programs/systems using machine learning.He regularly publishes at conferences such as CAV and TACAS.His paper titled "When simulation meets antichains (for checking language inclusion of NFA's)" won the best theory paper award at ETAPS 2010. He co-chaired the Infinity 2010 workshop at Singapore and served as PC member in conferences such as FM, APLAS, ICTAC.
Ahmed Bouajjani, Univ. Paris Diderot (Paris 7)
Linearizability Checking: Reductions to State Reachability
We address the issue of verifying the correctness of libraries of concurrent data structures. We consider the problem of checking whether given implementation is linearisable w.r.t. a sequential abstract specification of the data structure. We overview complexity and decidability results concerning this problem in general, and show cases where efficient reductions of this problem to state reachability problems are possible.
The talk is based on joint work with Micheal Emmi, Constantin Enea, and Jad Hamza.
Biography: Ahmed Bouajjani got his PhD in 1989 from the Univ. of Grenoble, and then his Habilitation in 1999 from the same university. He was associate professor in Grenoble and member of the Verimag lab. from 1990 to 1999. He is professor at the Univ. Paris Diderot (Paris 7) since 1999, and senior member of the "Institut Universitaire de France" since 2013. His main research interests are formal verification, model-checking, verification of infinite-state systems, program verification, automata and logic.
Zachary Kincaid, Princeton University
Incremental Proofs for Parameterized Programs
Incremental proof synthesis is a highly successful paradigm in software verification. The essential idea is that we can build correctness proofs for programs "one execution at a time" in a sample-prove-check loop: we sample an execution, augment our running proof so that it covers the sample, and then check that the running proof covers to all executions (if not, we generate a new sample and continue). In this talk, I will describe proof spaces, which are one method for adapting incremental proof synthesis to the setting of parameterized concurrent programs (programs in which the number of threads is finite but unbounded). I will show how proof spaces can be used to prove both safety and liveness properties.
Biography: Zachary Kincaid is currently completing his PhD at the University of Toronto, and will start as an Assistant Professor at Princeton University in Fall 2016. His research interests are in programming languages, program analysis and verification, and logic.
Xinyu Feng, University of Science and Technology of China
Reasoning about progress of concurrent objects
Progress of concurrent objects describes the termination of object methods. Depending on how the termination is affected by the concurrent environment, four different progress properties are commonly used, i.e., wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom. In this talk, we characterize the environment's interference over progress of objects from two different aspects, namely blocking and delay. We show the four different progress properties of concurrent objects can be classified according to the objects' different tolerance of blocking and delay. Then we propose a rely-guarantee style program logic to verify both linearizability and progress properties of concurrent objects. The logic also unifies the verification of all the four different progress properties. Applying the logic we have successfully verified progress properties of some representative algorithms, such as Treiber stack, Michael-Scott queue, DGLM queue, lock-coupling lists, optimistic lists, and lazy lists.
This is joint work with Hongjin Liang (USTC) and Zhong Shao (Yale).
Biography: Xinyu Feng is a professor in computer science at University of Science and Technology of China (USTC). He got his PhD degree at Yale University in 2007. Then he worked as a research assistant professor at Toyota Technological Institute at Chicago (TTIC) from 2007 to 2010. He joined USTC in 2010. His main research interest is about formal program verification and theories of programming languages. In particular, he is interested in developing theories, programming languages and tools to build formally certified system software, with rigorous guarantees of safety and correctness.
The rise of multicore CPUs, manycore GPUs, and other heterogeneous accelerator devices, presents exciting new opportunities for building more efficient computing systems. But with these opportunities comes a challenge: concurrent programming is notoriously difficult, and advances in analysis, programming and verification in the context of concurrency are required to meet this challenge.
There has been a surge of concurrency-related research activity from different viewpoints, such as the rethinking of programming abstractions and memory models; standardization and formalization of commonly used APIs and libraries; and investigating new forms of hardware support for parallel processing. While developing tools for verifying and debugging concurrent systems has been an important theme in the verification community for some time, we believe that formal verification research can go beyond checking existing code and systems, and play a role in identifying suitable abstractions for concurrency.
The goal of the annual (EC)2 workshop is thus to bring together researchers from the verification and program analysis community with experts who are involved, on the one hand, in developing multicore architectures, programming languages, or concurrency libraries, and on the other hand, in distributed computing and concurrency theory. Ultimately, such a diverse environment should stimulate incubation of ideas leading to future concurrent system design an verification tools that are essential in the multicore era.
We plan to have a diverse program, including invited talks, contributed talks, tutorials, and ample time for discussion. This is an informal workshop with no published proceedings. However, we will update this website to include talk abstracts and slides.
|Submission deadline:||May 20, 2016|
|Notification of acceptance:||May 27, 2016|
|Final version due||June 10, 2016|
|Workshop:||July 18, 2016|
Please submit a talk abstract through Eaychair here.
We do not have strict formatting guidelines. Prepare a 2-5 page talk abstract or a position paper in PDF format. The title and the name of the authors should appear at the top of the first page. At least one author of each submission is expected to register and attend to present the work.
Please use the CAV 2016 website to register for the workshop.