2001 Technical Reports

Report 2001-1. Abstraction and refinement for model checking inconsistent systems by Michael Huth and Shekhar Pradhan
Abstract: We stress the importance of refinement and abstraction notions and their restricted but well understood soundness in conventional model checking. We then explain why such notions should be central to the analysis of systems with multiple points of views. In particular, they can guide us in settling design questions such as the semantics of negation, and the production of valuable debugging information. Slides for the above paper

Report 2001-2. A pattern-based approach to developing concurrent programs in UML (Part 1) by Masaaki Mizuno

Report 2001-3. A pattern-based approach to developing concurrent programs in UML (Part 2) by Masaaki Mizuno

Report 2001-4. Expressing Checkable Properties of Dynamic Systems: The Bandera Specification Language by James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby

Report 2001-5. Symmetric Model Checking for Object-Based Programs by Radu Iosif
Abstract: Detecting symmetries in the structure of systems is a well known technique falling in the class of bisimulation (strongly) preserving state space reductions. Previous work in applying symmetries to aid model checking focuses mainly on process topologies and user specified data types. We applied the symmetry framework to model checking object-based programs that manipulate dynamically created objects, and developed a polynomial-time heuristic for finding the canonical representative of a symmetry equivalence class. The strategy was implemented in the object-based model checker dSPIN and some experiments, yielding encouraging results, have been carried out.

Report 2001-6. Invariant Consistency: A Mechanism for Inter-process Ordering in Distributed Shared Memory Systems by Gurdip Singh
Abstract: In a distributed shared memory (DSM) system, multiple copies of a shared variable may have to be maintained (in caches) to improve performance. Several notions of consistency have been proposed to provide a consistent view of the shared memory. A consistency notion imposes constraints on the order in which updates to shared variables are made visible to various processes. A constraint may restrict the sequence in which updates from the same process are made visible to other processes. We classify such constraints as "intra-process constraints" and many existing consistency notions provide flexible mechanisms to specify such constraints. We may also need to specify "inter-process" constraints to restrict the sequence in which updates issued by different processes are made visible.

In this paper, we propose the notion of invariant consistency that allows specification of such inter-process constraints. For this propose, we allow a programmer to label program operations and specify an invariant I constraining the execution of labeled operations at different processes. The implementation of invariant consistency ensures that the labeled operations are made visible in an order that satisfies I. We show that invariant consistency simplifies programming as it eliminates application-level synchronization code to enforce inter-process constraints. We show that inter-process ordering can be done more efficiently via invariant consistency as compared to application-level synchronization. We also give an implementation of invariant consistency that involves a mechanical translation of invariants to synchronization code.

Report 2001-7. Enhancing Real-time Event Service for Synchronization in Object Oriented Distributed Systems by Gurdip Singh, Bob Maddula and Qiang Zeng
Abstract: Distributed object computing middleware such as CORBA, RMI, and DCOM have gained wide acceptance and has shielded programmers from many tedious and error-prone aspects of distributed programming. In particular, CORBA Event Service has been used extensively in embedded systems. In this paper, we propose an aspect oriented approach to develop synchronization code for distributed systems that use event service as the underlying communication middleware. Our approach is to factor out synchronization as a separate aspect, synthesize synchronization code and then compose it with the functional code. To implement synchronization efficiently using the event service, we propose enhancements to the semantics of the event service. Specifically, we define the notion of condition events and exactly k semantics. We describe the implementation of the enhancements on the Tao's Real-Time Event Service. We present experimental results to demonstrate that the enhanced event service leads to more efficient implementation of synchronization.