Future contracts

ABSTRACT

Many recent research projects focus on language support for behavioral software contracts, that is, assertions that govern the boundaries between software building blocks such as procedures, classes, or modules. Contracts primarily help locate bugs in programs, but they also tend to affect the performance of the program, especially as they become complex.

In this paper, we introduce future contracts and parallel contract checking: software contracts annotated with future are checked in parallel with the main program, exploiting the now-common multiple-core architecture. We present both a model and a prototype implementation of our language design. Our model comprises a higher-order imperative language and we use it to prove the correctness of our design. Our implementation is robust enough to measure the performance of reasonably large benchmarks, demonstrating that the use of future contracts can lead to significant performance improvements.

REFERENCES

• 1: P. Avgustinov, J. Tibble, and O. de Moor. Making trace monitors feasible. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 589--608, 2007.
• 2: M. Barnett, K. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 2004, LNCS vol. 3362,
• 3: Springer, 2004. F. Chen and G. Roşu. Mop: an efficient and generic runtime verification framework. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications,pages 569--588, 2007.
• 4: C. Dimoulas and M. Wand. The aggregate update problem. In International Conference on Verification, Model Checking and Abstract Interpretation, pages 44--58, 2009.
• 5: A. Duncan and U. Hoelzle. Adding Contracts to Java with Handshake. Technical report, Santa Barbara, CA, USA, 1998.
• 6: M. Feeley. An efficient and general implementation of futures on large scale shared--memory multiprocessors. PhD thesis,Brandeis University, 1993.
• 7: M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, pages 235--271, 1992.
• 8: R. Findler and M. Blume. Contracts as Pairs of Projections. In International Symposium in Functional and Logic Programming,pages 226--241, 2006.
• 9: R. Findler and M. Felleisen. Contracts for higher-order functions. In ACM SIGPLAN International Conference on Functional Programming, pages 48--59, 2002.
• 10: R. Findler, J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi, P. Steckler, and M. Felleisen. DrScheme: A programming environment for scheme. Journal of Functional Programming, 12:369--388, 2002.
• 11: R. Findler, S. Guo, and A. Rogers. Lazy contract checking for immutable data structures. In International Symposium on Implementation and Application of Functional Languages, pages 22--34, 2007.
• 12: C. Flanagan and M. Felleisen. The semantics of future and an application. Journal of Functional Programming, 9(1):1--31, 1999.
• 13: M. Flatt. PLT MzScheme: Language manual. Technical Report PLT-TR2009-reference-v4.1.4, PLT Scheme Inc., 2009. http://www.plt--scheme.org/techreports/.
• 14: B. Gomes, D. Stoutamire, B. Vaysman, and H. Klawitter. A Language Manual for Sather 1.1, 1996.
• 15: R. Halstead. Implementation of Multilisp: Lisp on a multiprocessor. In ACM Symposium on LISP and Functional Programming,pages 9--17, 1984.
• 16: K. Havelund and G. Ros¸u. Monitoring Java Programs with Java PathExplorer. Technical report, 2001.
• 17: M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008.
• 18: R. Holt, P. Matthews, J. Rosselet, and J. Cordy. The Turing programming language: design and definition. Prentice-Hall, Inc.,Upper Saddle River, NJ, USA, 1987.
• 19: M. Karaorman, U. Holzle, and J. Bruno. jContractor: A Reflective Java Library to Support Design by Contract. Technical report, Santa Barbara, CA, USA, 1999.
• 20: M. Kim, M. Viswanathan, S. Kannan, I. Lee, and O. Sokolsky. Java-Mac: A Run-Time Assurance Approach for Java Programs. Formal Methods in Systems Design, 24(2):129--155, 2004.
• 21: M. Kölling and J. Rosenberg. Blue: Language Specification, version 0.94, 1997.
• 22: R. Kramer. iContract -- The Java(tm) design by Contract(tm) Tool. In Technology of Object-Oriented Languages and Systems, page 295, 1998.
• 23: G. Leavens, K. Leino, E. Poll, C. Ruby, and B. Jacobs. JML: notations and tools supporting detailed design in Java. In Object-Oriented Programming, Systems, Languages, and Applications Companion, pages 105--106, 2000.
• 24: D. Luckham and F. Von Henke. An Overview of Anna, a Specification Language for Ada. IEEE Software, 2(2):9--22, 1985. B. Meyer. Eiffel: The Language. Prentice Hall, 1992.
• 25: B. Meyer. Object-oriented Software Construction. Prentice Hall,1988.
• 26: D. Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15:1053--1058, 1972.
• 27: R. Ploesch and J. Pichler. Contracts: From Analysis to C++ Implementation. In Technology of Object-Oriented Languages and Systems, page 248, 1999.
• 28: A. Pnueli. The temporal logic of programs. In Symposium on the Foundations of Computer Science, pages 46--57, Providence, Rhode Island, 1977.
• 29: J. Reppy. Concurrent programming in ML. Cambridge University Press, New York, NY, USA, 1999. ISBN 0-521-48089-2.
• 30: D. Rosenblum. A Practical Approach to Programming With Assertions. IEEE Transactions on Software Engineering, 21(1):19--31, 1995.
• 31: O. Shivers. Control-Flow Analysis of Higher-Order Languages, or Taming Lambda. PhD thesis, Carnegie Mellon University, 1991.
• 32: K. Zee, V. Kuncak, and M. Rinard. Runtime Checking for Program Verification Systems. In Runtime Verification, pages 202--213,2007.

INDEX TERMS

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

General Terms:
Design, Reliability

Keywords:
behavioral specifications, contracts, higher-order functions, software reliability