Take a look at the new version of this page: [ beta version ]. Tell us what you think.

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: Pavel Avgustinov , Julian Tibble , Oege de Moor, Making trace monitors feasible, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 2: M. Barnett, K. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 2004, LNCS vol. 3362,
• 3: Feng Chen , Grigore Roşu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 4: Christos Dimoulas , Mitchell Wand, The Higher-Order Aggregate Update Problem, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, December 18-20, 2008, Savannah, GA [doi>10.1007/978-3-540-93900-9_8]
• 5: A. Duncan and U. Hoelzle. Adding Contracts to Java with Handshake. Technical report, Santa Barbara, CA, USA, 1998.
• 6: Marc Feeley, An efficient and general implementation of futures on large scale shared-memory multiprocessors, Brandeis University, Waltham, MA, 1993
• 7: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 8: R. Findler and M. Blume. Contracts as Pairs of Projections. In International Symposium in Functional and Logic Programming,pages 226--241, 2006.
• 9: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 10: Robert Bruce Findler , John Clements , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Paul Steckler , Matthias Felleisen, DrScheme: a programming environment for Scheme, Journal of Functional Programming, v.12 n.2, p.159-182, March 2002 [doi>10.1017/S0956796801004208]
• 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 , Mattias Felleisen, The semantics of future and an application, Journal of Functional Programming, v.9 n.1, p.1-31, January 1999 [doi>10.1017/S0956796899003329]
• 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: Robert H. Halstead, Jr., Implementation of multilisp: Lisp on a multiprocessor, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.9-17, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802017]
• 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: Richard C. Holt , Philip A. Matthews , J. Alan Rosselet , James R. Cordy, The Turing programming language: design and definition, Prentice-Hall, Inc., Upper Saddle River, NJ, 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: Moonzoo Kim , Mahesh Viswanathan , Sampath Kannan , Insup Lee , Oleg Sokolsky, Java-MaC: A Run-Time Assurance Approach for Java Programs, Formal Methods in System Design, v.24 n.2, p.129-155, March 2004 [doi>10.1023/B:FORM.0000017719.43755.7c]
• 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, Proceedings of the Technology of Object-Oriented Languages and Systems, p.295, August 03-07, 1998
• 23: Gary T. Leavens , Clyde Ruby , K. Rustan , M. Leino , Erik Poll , Bart Jacobs, JML (poster session): notations and tools supporting detailed design in Java, Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), p.105-106, January 2000, Minneapolis, Minnesota, United States [doi>10.1145/367845.367996]
• 24: D. C. Luckham , F. W. Von Henke, An Overview of Anna, a Specification Language for Ada, IEEE Software, v.2 n.2, p.9-22, March 1985 [doi>10.1109/MS.1985.230345]
• 25: Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 26: D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
• 27: Reinhold Ploesch , Josef Pichler, Contracts: From Analysis to C++ Implementation, Proceedings of the Technology of Object-Oriented Languages and Systems, p.248, August 01-05, 1999
• 28: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, p.46-57, September 30-October 31, 1977
• 29: John H. Reppy, Concurrent programming in ML, Cambridge University Press, New York, NY, 1999
• 30: David S. Rosenblum, A Practical Approach to Programming With Assertions, IEEE Transactions on Software Engineering, v.21 n.1, p.19-31, January 1995 [doi>10.1109/32.341844]
• 31: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 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