Szumo: Synchronization Contracts for Object-Oriented Languages

Introduction

The expressive power afforded by the use of concurrency comes at the expense of increased complexity. Without proper synchronization, concurrent access to shared objects can lead to race conditions, and incorrect synchronization logic can lead to starvation and/or deadlock. Moreover, concurrency confounds the development of reusable software modules because synchronization policies and decisions are difficult to localize into a single software module. Nowhere is this complexity more evident than in multi-threaded applications in which concurrent threads operate on shared data. Whereas parallel and distributed systems are becoming increasingly important, the safe and reliable use of concurrency in multi-threaded shared-memory systems has emerged as a fundamental and pervasive engineering concern, similar in nature to safety, efficiency, and scalability.

The Synchronization Units Model (Szumo) is a powerful model of synchronization contracts for object-oriented languages that addresses this complexity. In lieu of writing low-level code to acquire and release shared objects, programmers declare synchronization contracts in a module's interface. The contracts declare the circumstances under which the modules in a program require exclusive use of shared objects in a form that permits automated inference of how to synchronize processes in using these objects. At run time, a thread middleware negotiates the contracts on behalf of processes, ensuring that the contracts of all modules are met while simultaneously guarding against data races and deadlocks that can feasibly be avoided. Separating concurrency concerns from functional code simplifies programming, and localizing concurrency concerns in module interfaces simplifies reasoning.

Szumo was originally named The Universe Model and was developed by Dr. Reimer Behrends as part of his PhD research.

Personnel

Publications

• On Mechanisms for Deadlock Avoidance in SIP Servlet Containers
  • Appears in Proceedings of Principles, Systems, and Applications of IP Telecommunications (IPTComm'08)
  • Y. Huang, L. K. Dillon, and R. E. K. Stirewalt
• Using Formal Models to Objectively Judge Quality of Multi-Threaded Programs in Empirical Studies
  • Appears in Proceedings of the ICSE Workshop on Models in Software Engineering (MiSE'08), Leipzig, Germany, May 2008
  • L. K. Dillon, R. E. K. Stirewalt, Eileen T. Kraemer, Shaohua Xie, and Scott D. Fleming
• A Model-based Design-for-Verification Approach to Checking for Deadlock in Multi-Threaded Applications
  • Appears in International Journal of Software Engineering and Knowledge Engineering 17(2):207-230, 2007
  • Beata Sarna-Starosta, R. E. K. Stirewalt, and Laura K. Dillon
• Using Program Families for Maintenance Experiments
  • Appears in Proc. of the First Workshop on Assessment of Contemporary Modularization Techniques (ACoM.07), May 2007
  • Scott D. Fleming, R. E. K. Stirewalt, and L. K. Dillon
• Contracts and Middleware for Safe SOA Applications
  • Appears in Proc. of the International Workshop on Systems Development in SOA Environments, May 2007
  • Beata Sarna-Starosta, R. E. K. Stirewalt, and Laura K. Dillon
• Separating Synchronization Concerns with Frameworks and Generative Programming
  • S. D. Fleming, R. E. K. Stirewalt, L. K. Dillon, and B. Sarna-Starosta
  • Computer Science and Engineering Technical Report CSE-MSU-06-34
• Developing an Alloy Framework akin to OO Frameworks
  • L. K. Dillon, R. E. K. Stirewalt, B. Sarna-Starosta, and S. D. Fleming
  • Appears in Proc. of the First Alloy Workshop, November, 2006.
• Using Views to Specify a Synchronization Aspect for Object-Oriented Languages
  • R. E. K. Stirewalt, L. K. Dillon, and R. Behrends
  • Appears in Proc. of the 16^th International Z User Meeting, Columbia, Maryland, April 2006.
• A Model-Based Design-for-Verification Approach to Checking for Deadlock in Multi-Threaded Applications
  • B. Sarna-Starosta, R. E. K. Stirewalt, and L. K. Dillon
  • Appears in Proc of the 18^th International Conference on Software Engineering and Knowledge Engineering, San Francisco, July 2006
• A Component-Oriented Model for the Design of Safe Multi-threaded Applications
  • R. Behrends, R. E. K. Stirewalt, and L. K. Dillon
  • Appears in Proc. of the ACM SIGSOFT Symposium on Component Based Software Engineering, St. Louis, May 2005.
• Safe and Reliable use of Concurrency in Multi-Threaded Shared-Memory Systems
  • L. K. Dillon, R. Behrends, and R. E. K. Stirewalt
  • Appears in 29th Annual IEEE/NASA Software Engineering Workshop, Greenbelt, MD, April 2005
• Avoiding Serialization Vulnerabilities through the use of Synchronization Contracts
  • R. Behrends, R. E. K. Stirewalt, and L. K. Dillon
  • Appears in Proc. of the ASE Workshop on Specification and Automated Processing of Security Requirements, September 2004

• Designing and Implementing a Model of Synchronization Contracts in Object-Oriented Languages
  • R. Behrends
  • PhD Thesis, Michigan State University, December 2003

• The Universe Model: An approach for improving the modularity and reliability of concurrent programs
  • R. Behrends and R. E. K. Stirewalt
  • Appears in Proc. of ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE'2000)

Software

• Szumo/C++ An experimental C++-based programming system. Contains SzumoFrame and SzumoSzep.

• Szumo/Eiffel: An experimental compiler for the Eiffel language extended to support Szumo contracts.
  • Requires Ruby (v1.8.0 or later).
  • Language extensions are documented in chapter 8 of the dissertation above.
  • Currently runs on Linux, Solaris, and Mac OS X, but should be portable to other operating systems with relatively little effort. Portability of the compiler and runtime system is constrained only by the somewhat limited portability of POSIX threads (specifically, the generally broken implementation of sem_timedwait() and pthread_cond_timedwait() in most libraries) and the platforms that support the off-the-shelf conservative garbage collector that the runtime system employs.
  • The Linux/x86 implementation contains some assembly-language optimizations (using the processor's built-in compare-and-swap instruction), which do not port cleanly to other architectures. While they are not necessary, they provide non-negligible performance benefits. They are not enabled by default, but are switched on by #defines in runtime/runtime.c
  • Compiler has only limited support for incremental compilation, which may lead to large turnaround times for large programs.
• Reference implementation of run-time system written in Ruby and mirroring the pseudocode in the thesis above. Note: does not support synchronization constraints (which are a compile-time feature).