Abstract Interpretation against Races

• Autorzy: Barbuti R. , Cataudella S. , Tesei L.
• Języki publikacji: EN

Abstrakty

EN

In this paper we investigate the use of abstract interpretation techniques for statically preventing race conditions. To this purpose we enrich the concurrent object calculus concV by annotating terms with the set of ``locks'' owned at any time. We use an abstract form of the object calculus to check the absence of race conditions. We show that abstract interpretation is more flexible than type analyses, and it allows to certify as ``race free'' a larger class of programs.

Słowa kluczowe

EN

calculus; mathematical function; mathematical analysis; computer software; abstract

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 67--79
• Opis fizyczny: Bibliogr. 15 poz.,tab.

Twórcy

autor

Barbuti R.

• Dipartimento di Informatica, Universita di Pisa, Via F. Buonarroti, 2, 56127 Pisa, Italy

autor

Cataudella S.

• Dipartimento di Informatica, Universita di Pisa, Via F. Buonarroti, 2, 56127 Pisa, Italy

autor

Tesei L.

• Dipartimento di Informatica, Universita di Pisa, Via F. Buonarroti, 2, 56127 Pisa, Italy

Bibliografia

• [1] Martin Abadi. and Luca Cardelli. A Theory’ of Objects. Springer, 1996.
• [2] Jonathan Aldrich, Craig Chambers, Emin Giin Sirer, and Susan J. Eggers. Static Analyses for Eliminating Unnecessary Synchronization from Java Programs. Static Analysis Symposium (SAS) 1999. 19-38.
• [3] Juan Bicarregui, Kevin Lano, and T. S. E. Maibaum. Formalizing Object-Oriented Models in the Object Calculus. ECOOP Workshops 1997. Lecture Notes in Computer Science 1357. Springer, 1998. 155-160.
• [4] Chandrasekhar Boyapati. and Martin C. Rinard: A Parameterized Type System for Race-Free Java Programs. ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOP-SLA). SIGPLAN Notices 36(11), 2001. 56-69.
• [5] Chandrasekhar Boyapati, Robert Lee, and Martin C. Rinard. Ownership types for safe programming: preventing data races and deadlocks. ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA), SIGPLAN Notices 37(11), 2002. 211-230.
• [6] Patrick Cousot, and Radhia Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2, 1992.511-547.
• [7] Patrick Cousot. Abstract Interpretation. ACM Computing Sun’eys, 28, 1996. 324-328.
• [8] Jos Luiz Fiadeiro, and T. S. E. Maibaum. Describing. Structuring and Implementing Objects. Foundations of Object Oriented Languages. Lecture Notes in Computer Science 489, Springer, 1991.
• [9] Kathleen Fisher. Furio Honsell, and John C. Mitchell. A lambda Calculus of Objects and Method Specialization. Nordic Journal of Computing 1, 1994. 3-37.
• [10] Cormac Flanagan, and Martin Abadi. Types for Safe Locking. 8th European Symposium on Programming (ESOP), Lecture Notes in Computer Science 1576, Springer, 1999. 91-108.
• [11] Cormac Flanagan, and Martin Abadi. Object Types against Races. 10th International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1664, Springer, 1999. 288-303.
• [12] James Gosling, William N. Joy, and Guy L. Steele Jr. The Java Language Specification. Addison-Wesley, 1996.
• [13] Andrew D. Gordon, and Paul D. Hankin. A Concurrent Object Calculus: Reduction and Typing. Electronic Notes in Theoretical Computer Science (ENTCS), 16. 1998.
• [14] Kohei Honda, and Mario Tokoro. An Object Calculus for Asynchronous Communication. ECOOP 1991. Lecture Notes in Computer Science 512, Springer, 1991. 133-147.
• [15] Robert H. B. Netzer, and Barton P. Miller. What Are Race Conditions? Some Issues and Formalizations. ACM Letters on Programming Languages and Systems (LOPLAS), 1, 1992. 74-88.