The Taub Faculty of Computer Science Events and Talks

In the last two decades, program verification and testing have gone a long way from a concept to practical tools which can be applied to real software. In this work, we developed practical techniques for testing and verifying atomicity of composed concurrent operations. The techniques have been implemented in a tool (COLT) and successfully applied to uncover many bugs in real software. In fact, the Java library is currently being modified to avoid some of the bugs found by COLT. The effectiveness of COLT comes from an understanding of the interface requirements and using them to shorten the executed traces, avoiding superfluous traces which cannot uncover new violations. COLT can also effectively prove the absence of atomicity violations for composed concurrent map operations. The main idea is to bound the number of keys and values that must be explored. This relies on restricting composed operations to be data-independent. That is, the control-flow of the composed operation does not depend on specific input values. While verifying data-independence is undecidable in the general case, we provide simple sufficient conditions that can be used to establish a composed operation as data-independent. We show that for the common case of concurrent maps, data-independence reduces the hard problem of verifying linearizability into a verification problem that can be solved efficiently using a bounded number of keys and values.