1. 5

Abstract: “The central notion of this paper is that of contracts for concurrency, allowing one to capture the expected atomicity of sequences of method or service calls in a concurrent program. The contracts may be either extracted automatically from the source code, or provided by developers of libraries or software modules to reflect their expected usage in a concurrent setting. We start by extending the so-far considered notion of contracts for concurrency in several ways, improving their expressiveness and enhancing their applicability in practice. Then, we propose two complementary analyses—a static and a dynamic one—to verify programs against the extended contracts. We have implemented both approaches and present promising experimental results from their application on various programs, including real-world ones where our approach unveiled previously unknown errors.”

Uses ANaConDA Framework.


  2. 3

    Hey @hwayne, might want to add this quote to the list of stuff made easy with contracts and formal tooling that might be really hard with testing:

    “…an older version of the Chrome browser (version 6.0.472.35) containing a known atomicity violation leading to an assertion failure. As this error can be described using a contract, we tried our tool to find the error. The experiment was successful, showing that our tool can handle even large programs. Interestingly, to find the error without the on-the-fly approach, one would need to store a trace with more than 17 million method calls (about 1.6 GB of data) while the on-thefly method needed about 10 MB of data only.”

    My emphasis added. That’s more extreme than Amazon’s example for TLA+ with 30+ steps. Analysis of the 7.5 Mloc software for concurrency errors took 49.12 seconds.

    1. 2

      The bad news is I didn’t get an alert when you tagged me

      The good news is I clicked on the story anyway :D

      1. 1

        Yeah, that’s good news haha.