nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

The Essence of Higher-Order Concurrent Separation Logic

verfasst von : Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Concurrent separation logics (CSLs) have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids (PCMs) and invariants. However, the realization of these concepts in Iris still bakes in several complex mechanisms—such as weakest preconditions and mask-changing view shifts—as primitive notions.

In this paper, we take the Iris story to its (so to speak) logical conclusion, applying the reductionist methodology of Iris to Iris itself. Specifically, we define a small, resourceful base logic, which distills the essence of Iris: it comprises only the assertion layer of vanilla separation logic, plus a handful of simple modalities. We then show how the much fancier logical mechanisms of Iris—in particular, its entire program specification layer—can be understood as merely derived forms in our base logic. This approach helps to explain the meaning of Iris’s program specifications at a much higher level of abstraction than was previously possible. We also show that the step-indexed “later” modality of Iris is an essential source of complexity, in that removing it leads to a logical inconsistency. All our results are fully formalized in the Coq proof assistant.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel The Power of Non-determinism in Higher-Order Implicit Complexity

Nächstes Kapitel Comprehending Isabelle/HOL’s Consistency

The full judgment is of the shape \(\varGamma \mid P\vdash Q\), where \(\varGamma \) assigns types to free variables. However, since \(\varGamma \) only plays a role in the rules for quantifiers, we omit it.

Implicitly, they also have an invalid element

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54434-1_26/442829_1_En_26_IEq281_HTML.gif

, for composition of overlapping sets.

The Iris 3.0 documentation and Coq development. Available on the Iris project website at: http://iris-project.org

Appel, A., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. TOPLAS 23(5), 657–683 (2001)CrossRef

Appel, A., Melliès, P.-A., Richards, C., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL (2007)

Appel, A.W. (ed.): Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)MATH

Ashcroft, E.A.: Proving assertions about parallel programs. JCSS 10(1), 110–135 (1975)MathSciNetMATH

Beringer, L., Stewart, G., Dockins, R., Appel, A.W.: Verified compilation for shared-memory C. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 107–127. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_7CrossRef

Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: 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). doi:10.1007/3-540-44898-5_4CrossRef

Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207–231. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44202-9_9CrossRef

10.

Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), 453–457 (1975)MathSciNetCrossRef

11.

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). doi:10.1007/978-3-642-14107-2_24CrossRef

12.

Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363–377. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00590-9_26CrossRef

13.

Dreyer, D., Neis, G., Rossberg, A., Birkedal, L.: A relational modal logic for higher-order stateful ADTs. In: POPL (2010)

14.

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). doi:10.1007/978-3-540-78739-6_27CrossRef

15.

Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14–26 (2001)

16.

Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL (2011)

17.

Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: ICFP, pp. 256–269 (2016)

18.

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637–650 (2015)

19.

Kock, A.: Monads on symmetric monoidal closed categories. Arch. Math. 21(1), 1–10 (1970)MathSciNetCrossRef

20.

Kock, A.: Strong functors and monoidal monads. Arch. Math. 23(1), 113–120 (1972)MathSciNetCrossRef

21.

Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL, pp. 205–217 (2017)

22.

Krogh-Jespersen, M., Svendsen, K., Birkedal, L.: A relational model of types-and-effects in higher-order concurrent separation logic. In: POPL (2017)

23.

Nakano, H.: A modality for recursion. In: LICS (2000)

24.

O’Hearn, P.: Resources, concurrency, and local reasoning. TCS 375(1), 271–307 (2007)MathSciNetCrossRef

25.

O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symb. Logic 5(2), 215–244 (1999)MathSciNetCrossRef

26.

Parkinson, M.: The next 700 separation logics. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 169–182. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15057-9_12CrossRef

27.

Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77–87 (2015)

28.

Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_9CrossRef

29.

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). doi:10.1007/978-3-642-37036-6_11CrossRef

30.

Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377–390 (2013)

Titel: The Essence of Higher-Order Concurrent Separation Logic
verfasst von: Robbert Krebbers
Ralf Jung
Aleš Bizjak
Jacques-Henri Jourdan
Derek Dreyer
Lars Birkedal
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54434-1_26

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"