Research Outputs

Permanent URI for this communityhttps://hdl.handle.net/20.500.14288/2

Browse

Filters

2010 - 20152

Advanced Search

Filter by

Settings

Quartile: search.filters.quartile.Q4Subject: search.filters.subject.Electrical electronics engineering

Search Results

Now showing 1 - 2 of 2
  • Placeholder
    PublicationMetadata only
    Automated and modular refinement reasoning for concurrent programs
    (Springer International Publishing Ag, 2015) Hawblitzel, Chris; Petrank, Erez; Qadeer, Shaz; Department of Computer Engineering; Taşıran, Serdar; Faculty Member; Department of Computer Engineering; College of Engineering; N/A
    We present CIVL, a language and verifier for concurrent programs based on automated and modular refinement reasoning. CIVL supports reasoning about a concurrent program at many levels of abstraction. Atomic actions in a high-level description are refined to fine-grain and optimized lower-level implementations. A novel combination of automata theoretic and logic-based checks is used to verify refinement. Modular specifications and proof annotations, such as location invariants and procedure pre- and post-conditions, are specified separately, independently at each level in terms of the variables visible at that level. We have implemented CIVL as an extension to the BOOGIE language and verifier. We have used CIVL to refine a realistic concurrent garbage collection algorithm from a simple high-level specification down to a highly-concurrent implementation described in terms of individual memory accesses.
  • Placeholder
    PublicationMetadata only
    Tressa: claiming the future
    (Springer, 2010) Qadeer, Shaz; N/A; N/A; Sezgin, Ali; Taşıran, Serdar; Researcher; Faculty Member; N/A; N/A; N/A; N/A
    Unlike sequential programs, concurrent programs have to account for interference on shared variables. Static verification of a desired property for such programs crucially depends on precisely asserting the conditions for interference. In a static proof system, in addition to program variables, auxiliary (history) variables summarizing the past of the program execution are used in these assertions. Capable of expressing reachability only, assertions (and history variables) are not as useful in the proofs of programs using optimistic concurrency. Pessimistic implementations which allow access to shared data only after synchronization (e.g. locks) guarantee exclusivity; optimistic concurrency implementations which check for interference after shared data is accessed abandon exclusivity in favor of performance. In this paper, we propose a new construct, tressa, to express properties, including interference, about the future of an execution. A tressa claim states a condition for reverse reachability from an end state of the program, much like an assert claim states a condition for forward reachability from the initial state of the program. As assertions employ history variables, tressa claims employ prophecy variables, originally introduced for refinement proofs. Being the temporal dual of history variables, prophecy variables summarize the future of the program execution. We present the proof rules and the notion of correctness of a program for two-way reasoning in a static setting: forward in time for assert claims, backward in time for tressa claims. We have incorporated our proof rules into the QED verifier and have used our implementation to verify a small but sophisticated algorithm. Our experience shows that the proof steps and annotations follow closely the intuition of the programmer, making the proof itself a natural extension of implementation.