Abstract
We present a case study of formal specification for the C\(^\sharp\) joins library, an advanced concurrent library implemented using both shared mutable state and higher-order methods. The library is specified and verified in HOCAP, a higher-order separation logic extended with a higher-order variant of concurrent abstract predicates.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Biering, B., Birkedal, L., Torp-Smith, N.: BI-Hyperdoctrines, Higher-order Separation Logic, and Abstraction. ACM TOPLAS (2007)
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Proceedings of POPL, pp. 259–270 (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Courtois, P.-J., Heymans, F., Parnas, D.L.: Concurrent Control with “Readers” and “Writers”. Commun. ACM 14(10), 667–668 (1971)
da Rocha Pinto, P., Dinsdale-Young, T., Dodds, M., Gardner, P., Wheelhouse, M.: A simple abstraction for complex concurrent indexes. SIGPLAN Not. 46(10), 845–864 (2011)
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: Compositional Reasoning for Concurrent Programs. In: Proceedings of POPL (2013)
Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent Abstract Predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)
Fournet, C., Gonthier, G.: The reflexive chemical abstract machine and the join-calculus. In: Proceedings of POPL (1996)
Fournet, C., Gonthier, G.: The Join Calculus: A Language for Distributed Mobile Programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 268–332. Springer, Heidelberg (2002)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local Reasoning for Storable Locks and Threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007)
Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)
Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011)
Jacobs, B.: Verified general barriers implementation, http://people.cs.kuleuven.be/~bart.jacobs/verifast/examples/barrier.c.html
Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Proceedings of POPL, pp. 271–282 (2011)
Krishnaswami, N.: Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis, Carnegie Mellon University (2012)
Krishnaswami, N., Birkedal, L., Aldrich, J.: Verifying Event-Driven Programs using Ramified Frame Properties. In: Proceedings of TLDI (2010)
O’Hearn, P.W.: Resources, Concurrency and Local Reasoning. Theor. Comput. Sci. 375(1-3), 271–307 (2007)
Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Cornell (1975)
Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Proceedings of POPL, pp. 247–258 (2005)
Russo, C.V.: The Joins Concurrency Library. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 260–274. Springer, Heidelberg (2007)
Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare Triples and Frame Rules for Higher-Order Store. LMCS, 7(3:21) (2011)
Svendsen, K., Birkedal, L., Parkinson, M.: Verifying Generics and Delegates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 175–199. Springer, Heidelberg (2010)
Svendsen, K., Birkedal, L., Parkinson, M.: Higher-order Concurrent Abstract Predicates. Technical report, IT University of Copenhagen (2012), http://www.itu.dk/people/kasv/hocap-tr.pdf
Svendsen, K., Birkedal, L., Parkinson, M.: Verification of the Joins Library in Higher-order Separation Logic. Technical report, IT University of Copenhagen (2012), http://www.itu.dk/people/kasv/joins-tr.pdf
Svendsen, K., Birkedal, L., Parkinson, M.: Impredicative Concurrent Abstract Predicates. Under submission (2013)
Svendsen, K., Birkedal, L., Parkinson, M.: Modular Reasoning about Separation of Concurrent Data Structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 169–188. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Svendsen, K., Birkedal, L., Parkinson, M. (2013). Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library. In: Castagna, G. (eds) ECOOP 2013 – Object-Oriented Programming. ECOOP 2013. Lecture Notes in Computer Science, vol 7920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39038-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-39038-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39037-1
Online ISBN: 978-3-642-39038-8
eBook Packages: Computer ScienceComputer Science (R0)