We present a unified environment for running declarative specifications in the context of an imperative object-oriented programming language. Specifications are Alloy-like, written in first-order relational logic with transitive closure, and the imperative language is Java. By being able to mix imperative code with executable declarative specifications, the user can easily express constraint problems in place, i.e., in terms of the existing data structures and objects on the heap. After a solution is found, the heap is updated to reflect the solution, so the user can continue to manipulate the program heap in the usual imperative way. We show that this approach is not only convenient, but, for certain problems can also outperform a standard imperative implementation. We also present an optimization technique that allowed us to run our tool on heaps with almost 2000 objects.
Squander is a framework that provides a unified environment for writing declarative constraints and imperative statements in the context of a single program. This is particularly useful for implementing programs that involve computations that are relatively easy to specify but hard to solve algorithmically. In such cases, declarative constraints can be a natural way to express the core computation, whereas imperative code is a natural choice for reading the input parameters, populating the working data structures, setting up the problem, and presenting the solution back to the user. The ability to switch smoothly back and forth between declarative logic and imperative programming makes it possible to implement this kind of program more elegantly and with less effort on the programmer’s part.
project home page
full papers: ICSE 2011, Onward! 2009
Monday, May 30, 2011
Wednesday, May 25, 2011
Verification of Semantic Commutativity Conditions and Inverse Operations on Linked Data Structures
Our paper [1] presents 1) a new commutativity analysis technique that verifies sound and complete semantic commutativity conditions for linked data structures and 2) a new analysis for verifying inverse operations that undo the effect of previously executed operations on linked data structures.
Commuting operations play a critical role in many parallel computing systems. We present a new technique for verifying commutativity conditions, which are logical formulas that characterize when operations commute. Because our technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantically equivalent (but not identical) data structure states in different execution orders. We have used this technique to verify sound and complete commutativity conditions for all pairs of operations on a collection of linked data structure implementations, including data structures that export a set interface (ListSet and HashSet) as well as data structures that export a map interface (AssociationList, HashTable, and ArrayList). This effort involved the specification and verification of 765 commutativity conditions.
Many speculative parallel systems need to undo the effects of speculatively executed operations. Inverse operations, which undo these effects, are often more efficient than alternate approaches (such as saving and restoring data structure state). We present a new technique for verifying such inverse operations. We have specified and verified, for all of our linked data structure implementations, an inverse operation for every operation that changes the data structure state.
Together, the commutativity conditions and inverse operations provide a key resource that language designers and system developers can draw on to build parallel languages and systems with strong correctness guarantees.
[1] D. Kim and M. Rinard. Verification of Semantic Commutativity Conditions and Inverse Operations on Linked Data Structures. In PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011.
Commuting operations play a critical role in many parallel computing systems. We present a new technique for verifying commutativity conditions, which are logical formulas that characterize when operations commute. Because our technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantically equivalent (but not identical) data structure states in different execution orders. We have used this technique to verify sound and complete commutativity conditions for all pairs of operations on a collection of linked data structure implementations, including data structures that export a set interface (ListSet and HashSet) as well as data structures that export a map interface (AssociationList, HashTable, and ArrayList). This effort involved the specification and verification of 765 commutativity conditions.
Many speculative parallel systems need to undo the effects of speculatively executed operations. Inverse operations, which undo these effects, are often more efficient than alternate approaches (such as saving and restoring data structure state). We present a new technique for verifying such inverse operations. We have specified and verified, for all of our linked data structure implementations, an inverse operation for every operation that changes the data structure state.
Together, the commutativity conditions and inverse operations provide a key resource that language designers and system developers can draw on to build parallel languages and systems with strong correctness guarantees.
[1] D. Kim and M. Rinard. Verification of Semantic Commutativity Conditions and Inverse Operations on Linked Data Structures. In PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011.
Monday, May 16, 2011
Language-Independent Sandboxing of Just-In-Time Compilation and Self-Modifying Code
In our PLDI paper, we present an enabling technology for safely incorporating new language runtimes into the web browser:
When dealing with dynamic, untrusted content, such as on the Web, software behavior must be sandboxed, typically through use of a language like JavaScript. However, even for such specially-designed languages, it is difficult to ensure the safety of highly-optimized, dynamic language runtimes which, for efficiency, rely on advanced techniques such as Just-In-Time (JIT) compilation, large libraries of native-code support routines, and intricate mechanisms for multi-threading and garbage collection. Each new runtime provides a new potential attack surface and this security risk raises a barrier to the adoption of new languages for creating untrusted content.
Removing this limitation, our paper introduces general mechanisms for safely and efficiently sandboxing software, such as dynamic language runtimes, that make use of advanced, low-level techniques like runtime code modification. Our language-independent sandboxing builds on Software-based Fault Isolation (SFI), a traditionally static technique. We provide a more flexible form of SFI by adding new constraints and mechanisms that allow safety to be guaranteed despite runtime code modifications.
We have added our extensions to both the x86-32 and x86-64 variants of a production-quality, SFI-based sandboxing platform; on those two architectures SFI mechanisms face different challenges. We have also ported two representative language platforms to our extended sandbox: the Mono common language runtime and the V8 JavaScript engine. In detailed evaluations, we find that sandboxing slowdown varies between different benchmarks, languages, and hardware platforms. Overheads are generally moderate and they are close to zero for some important benchmark/platform combinations.
Friday, May 13, 2011
Detecting and Escaping Infinite Loops with Jolt!
Infinite loops are destructive to the usability of applications; in many cases the user may lose unsaved work or be unable to receive a complete output.
In our ECOOP paper we present Jolt, a system for detecting and escaping infinite loops at runtime. At a user's request, Jolt can attach to and monitor the execution of the program. Jolt checks if the program has entered an infinite loop in which the computation is making no progress at all---at the beginning of each loop iteration the program is in exactly the same state. If this is true, then Jolt offers the user the option to escape the loop by continuing execution of the program at the instruction that follows the loop.
In our case studies, Jolt was able to detect seven of the eight infinite loops that we found in common UNIX command-line utilities (ctags, grep, look, ping, and indent). For three of these eight loops, the strategy of escaping the loop also is the exact fix that the developers later implemented to fix the program. And for all of the loops, escaping an infinite loop proved to be more useful than terminating the program---it allowed the user to successfully recover functionality, by allowing the program to save temporary work and continue processing additional inputs.
For more information, check out the project page at
http://groups.csail.mit.edu/pac/jolt.
In our ECOOP paper we present Jolt, a system for detecting and escaping infinite loops at runtime. At a user's request, Jolt can attach to and monitor the execution of the program. Jolt checks if the program has entered an infinite loop in which the computation is making no progress at all---at the beginning of each loop iteration the program is in exactly the same state. If this is true, then Jolt offers the user the option to escape the loop by continuing execution of the program at the instruction that follows the loop.
In our case studies, Jolt was able to detect seven of the eight infinite loops that we found in common UNIX command-line utilities (ctags, grep, look, ping, and indent). For three of these eight loops, the strategy of escaping the loop also is the exact fix that the developers later implemented to fix the program. And for all of the loops, escaping an infinite loop proved to be more useful than terminating the program---it allowed the user to successfully recover functionality, by allowing the program to save temporary work and continue processing additional inputs.
For more information, check out the project page at
http://groups.csail.mit.edu/pac/jolt.
Subscribe to:
Posts (Atom)