Abstract
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional permissions with abstract predicates. As an example, we present a separation logic contract for iterators that prevents data races and concurrent modifications. Our program logic is presented in an algorithmic style: we avoid structural rules for Hoare triples and formalize logical reasoning about typed heaps by natural deduction rules and a set of sound axioms. We show that verified programs satisfy the following properties: data race freedom, absence of null-dereferences and partial correctness.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6) (2004)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: Formal Methods for Components and Objects (2005)
Bierhoff, K., Aldrich, J.: Modular typestate verification of aliased objects. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (2007)
Bornat, R., O’Hearn, P., Calcagno, C., Parkinson, M.: Permission accounting in separation logic. In: Principles of Programming Languages. ACM Press, New York (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)
Boyland, J.: Semantics of fractional permissions with nesting. Technical report, University of Wisconsin at Milwaukee (2007)
Boyland, J., Retert, W.: Connecting effects and uniqueness with adoption. In: Principles of Programming Languages (2005)
Boyland, J., Retert, W., Zhao, Y.: Iterators can be independent ”from” their collections. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (2007)
Chin, W., David, C., Nguyen, H., Qin, S.: Enhancing modular OO verification with separation logic. In: Principles of Programming Languages (2008)
Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Principles of Programming Languages (1999)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Programming Languages Design and Implementation (2001)
DeLine, R., Fähndrich, M.: Typestates for objects. In: European Conference on Object-Oriented Programming (2004)
Girard, J.-Y.: Linear logic: Its syntax and semantics. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. Cambridge University Press, Cambridge (1995)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Asian Programming Languages and Systems Symposium (2007)
Haack, C., Hurlin, C.: Resource usage protocols for iterators, http://www.cs.ru.nl/~chaack/papers/iterators.pdf
Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork/join. Technical Report 6430, INRIA (2008)
Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3) (2001)
Ishtiaq, S., O’Hearn, P.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (2001)
Krishnaswami, G.: Reasoning about iterators with separation logic. In: Specification and Verification of Component-Based Systems (2006)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Software Engineering Notes 31(3) (2006)
Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (1998)
O’Hearn, P.: Resources, concurrency and local reasoning. Theor. Comp. Science 375(1–3) (2007)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2) (1999)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Principles of Programming Languages, Venice, Italy. ACM Press, New York (2004)
Parkinson, M.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge (2005)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Principles of Programming Languages (2005)
Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Principles of Programming Languages (2008)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark. IEEE Press, Los Alamitos (2002)
Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol. 1782. Springer, Heidelberg (2000)
Wadler, P.: A taste of linear logic. In: Mathematical Foundations of Computer Science (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haack, C., Hurlin, C. (2008). Separation Logic Contracts for a Java-Like Language with Fork/Join. In: Meseguer, J., Roşu, G. (eds) Algebraic Methodology and Software Technology. AMAST 2008. Lecture Notes in Computer Science, vol 5140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79980-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-79980-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79979-5
Online ISBN: 978-3-540-79980-1
eBook Packages: Computer ScienceComputer Science (R0)