ACM Home Page
Please provide us with feedback. Feedback
Future contracts
Full text PdfPdf (409 KB)
Source
International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents
Coimbra, Portugal
SESSION: Concurrency table of contents
Pages 195-206  
Year of Publication: 2009
ISBN:978-1-60558-568-0
Authors
Christos Dimoulas  Northeastern University, Boston, MA, USA
Riccardo Pucella  Norhteastern University, Boston, MA, USA
Matthias Felleisen  Northeaster University, Boston, MA, USA
Sponsors
SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 8,   Downloads (12 Months): 8,   Citation Count: 0
Additional Information:

abstract   references   index terms  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599435
What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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.