Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. (English) Zbl 1346.68135
Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’15, Mumbai, India, January 12–18, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3300-9). 637-650 (2015).
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 03B70 | Logic in computer science |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
atomicity; compositional verification; fine-grained concurrency; higher-order logic; invariants; partial commutative monoids; separation logicReferences:
| [1] | Appendix and Coq development. http://plv.mpi-sws.org/iris. |
| [2] | M. Abadi and L. Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253-284, 1991. 10.1016/0304-3975(91)90224-P · Zbl 0728.68083 |
| [3] | A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009. 10.1145/1480881.1480925 |
| [4] | P. America and J. Rutten. Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci., 39(3):343-375, 1989. · Zbl 0717.18002 |
| [5] | E. A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10(1):110-135, 1975. 10.1016/S0022-0000(75)80018-3 · Zbl 0299.68013 |
| [6] | L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang. Step-indexed Kripke models over recursive worlds. In POPL, 2011. 10.1145/1926385.1926401 |
| [7] | E. Cohen, et al. Invariants, modularity, and rights. In PSI, 2009. 10.1007/978-3-642-11486-1_4 |
| [8] | P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. TaDA: A logic for time and data abstraction. In ECOOP, 2014. |
| [9] | T. Dinsdale-Young, L. Birkedal, P. Gardner, M. J. Parkinson, and H. Yang. Views: Compositional reasoning for concurrent programs. In POPL, 2013. 10.1145/2429069.2429104 · Zbl 1301.68099 |
| [10] | T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In ECOOP, 2010. |
| [11] | R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In APLAS, 2009. 10.1007/978-3-642-10672-9_13 |
| [12] | X. Feng. Local rely-guarantee reasoning. In POPL, 2009. 10.1145/1480881.1480922 |
| [13] | X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP, 2007. |
| [14] | I. Filipović, P. O’Hearn, N. Torp-Smith, and H. Yang. Blaming the client: On data refinement in the presence of pointers. In FACS, 2009. |
| [15] | M. Fu, Y. Li, X. Feng, Z. Shao, and Y. Zhang. Reasoning about optimistic concurrency using a program logic for history. In CONCUR, 2010. |
| [16] | D. Hendler, N. Shavit, and L. Yerushalmi. A scalable lock-free stack algorithm. In SPAA, 2004. 10.1145/1007912.1007944 |
| [17] | M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. TOPLAS, 12(3):463-492, 1990. 10.1145/78969.78972 |
| [18] | B. Jacobs. Personal communication, 2014. |
| [19] | B. Jacobs and F. Piessens. Expressive modular fine-grained concurrency specification. In POPL, 2011. 10.1145/1926385.1926417 |
| [20] | J. B. Jensen and L. Birkedal. Fictional separation logic. In ESOP, 2012. 10.1007/978-3-642-28869-2_19 |
| [21] | C. B. Jones. Tentative steps toward a development method for interfering programs. TOPLAS, 5(4):596-619, 1983. 10.1145/69575.69577 · Zbl 0517.68032 |
| [22] | N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In ICFP, 2012. 10.1145/2364527.2364536 |
| [23] | L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans.Comput., 28(9):690-691, 1979. 10.1109/TC.1979.1675439 · Zbl 0419.68045 |
| [24] | R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarse-grained concurrency. In POPL, 2013. 10.1145/2429069.2429134 |
| [25] | H. Liang and X. Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, 2013. 10.1145/2491956.2462189 |
| [26] | R. Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999. · Zbl 0942.68002 |
| [27] | A. Nanevski, R. Ley-Wild, I. Sergey, and G. A. Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP, 2014. |
| [28] | P. O’Hearn. Resources, concurrency, and local reasoning. TCS, 375(1):271-307, 2007. 10.1016/j.tcs.2006.12.035 · Zbl 1111.68023 |
| [29] | S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. CACM, 19(5):279-285, 1976. 10.1145/360051.360224 · Zbl 0322.68010 |
| [30] | A. Pilkiewicz and F. Pottier. The essence of monotonic state. In TLDI, 2011. 10.1145/1929553.1929565 |
| [31] | J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002. |
| [32] | F. Sieczkowski, A. Bizjak, Y. Zakowski, and L. Birkedal. Modular reasoning about concurrent higher-order imperative programs: a Coq tutorial. http://users-cs.au.dk/birke/modures/tutorial/index.html, 2014. |
| [33] | K. Svendsen and L. Birkedal. Impredicative concurrent abstract predicates. In ESOP, 2014. |
| [34] | A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP, 2013. 10.1145/2500365.2500600 · Zbl 1323.68386 |
| [35] | A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer. Logical relations for fine-grained concurrency. In POPL, 2013. 10.1145/2429069.2429111 |
| [36] | V. Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2007. |
| [37] | V. Vafeiadis and M. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, 2007. |
| [38] | D. Walker. Objects in the pi-calculus. Inf. Comput., 116(2):253-271, 1995. 10.1006/inco.1995.1018 · Zbl 0828.68043 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
