Scheduling-independent threads and exceptions in SHIM

ABSTRACT

Concurrent programming languages should be a good fit for embedded systems because they match the intrinsic parallelism of their architectures and environments. Unfortunately, typical concurrent programming formalisms are prone to races and nondeterminism, despite the presence of mechanisms such as monitors.In this paper, we propose SHIM, the core of a deterministic concurrent language, meaning the behavior of a program is independent of the scheduling of concurrent operations. SHIM does not sacrifice power or flexibility to achieve this determinism. It supports both synchronous and asynchronous paradigms-loosely and tightly synchronized threads-the dynamic creation of threads and shared variables, recursive procedures, and exceptions.We illustrate our programming model with examples including breadth-first-search algorithms and pipelines. By construction, they are race-free. We provide the formal semantics of SHIM and a pre-liminary implementation.

REFERENCES

• 1: Gregory R. Andrews , Fred B. Schneider, Concepts and Notations for Concurrent Programming, ACM Computing Surveys (CSUR), v.15 n.1, p.3-43, March 1983 [doi>10.1145/356901.356903]
• 2: C. Artho, K. Havelund, and A. Biere. High-level data races. In Proceedings of the Workshop on Verification and Validation of Enterprise Information Systems (VVEIS), pages 82--93, Angers, France, Apr. 2003.
• 3: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 4: A. Benveniste and G. Berry. The synchronous approach to reactive real-time systems. Proceedings of the IEEE, 79(9):1270--1282, Sept. 1991.
• 5: A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. L. Guernic, and R. de Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 91(1):64--83, Jan. 2003.
• 6: Gérard Berry, Preemption in Concurrent Systems, Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, p.72-93, December 15-17, 1993
• 7: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
• 8: F. Boussinot. FairThreads: mixing cooperative and preemptive threads in C. RR 5039, INRIA, 2003.
• 9: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 10: P. Brinch Hansen. The programming language Concurrent-Pascal. IEEE Transactions on Software Engineering, 1(2):199--207, June 1975.
• 11: Per Brinch Hansen, Monitors and Concurrent Pascal: a personal history, History of programming languages---II, ACM Press, New York, NY, 1996 [doi>10.1145/234286.1057814]
• 12: M. Burrows, K. Rustan, and M. Leino. Finding stale-value errors in concurrent programs. Technical Report 2002-004, Systems Research Center, Compaq, May 2002.
• 13: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 15: Stephen A. Edwards , Olivier Tardieu, SHIM: a deterministic model for heterogeneous embedded systems, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086277]
• 16: S. A. Edwards and O. Tardieu. SHIM: A deterministic model for heterogeneous embedded systems. IEEE Transactions on Very Large Scale Integrated (VLSI) Systems, 2006. To appear.
• 17: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 18: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 19: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 20: Cédric Fournet , Georges Gonthier, The Join Calculus: A Language for Distributed Mobile Programming, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, p.268-332, September 09-15, 2000
• 21: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 22: Jean D. Ichbiah , Bernd Krieg-Brueckner , Brian A. Wichmann , John G. P. Barnes , Olivier Roubine , Jean-Claude Heliard, Rationale for the design of the Ada programming language, ACM SIGPLAN Notices, v.14 n.6b, p.1-261, June 1979 [doi>10.1145/956653.956654]
• 23: INMOS Limited. occam 2 Reference Manual. Prentice Hall, 1988.
• 24: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 25: G. Kahn. The semantics of a simple language for parallel programming. In Information Processing 74: Proceedings of IFIP Congress 74, pages 471--475, Stockholm, Sweden, Aug. 1974. North-Holland.
• 26: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 27: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 28: Thomas Martyn Parks, Bounded scheduling of process networks, University of California at Berkeley, Berkeley, CA, 1996
• 29: G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Åarhus, Denmark, 1981.
• 30: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 31: The Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA. http://coq.inria.fr/doc/main.html.
• 32: Mandana Vaziri , Frank Tip , Julian Dolby, Associating synchronization constraints with data in an object-oriented language, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.334-345, January 11-13, 2006, Charleston, South Carolina, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Languages, Theory

Keywords:
deterministic model of computation, hardware/software codesign