Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Disjoint Polymorphism Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

A Higher-Order Logic for Concurrent Termination-Preserving Refinement

verfasst von : Joseph Tassarotti, Ralf Jung, Robert Harper

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
loading …

Abstract

Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.

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 Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Nächstes Kapitel Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Fußnoten
1
Setting aside issues of IO behavior.
 
2
This definition is simpler than the version found in Lehmann et al. [23], because there threads can be temporarily disabled, i.e., blocked and unable to take a step. In the languages we consider, threads can always take a step unless they have finished executing or have “gone wrong”.
 
3
The notation in Turon et al. [36] is different.
 
4
For the reader familiar with that work: we leave out subtyping and choice types. Also, we present an affine type system instead of a linear one.
 
5
Note that many of these assertions are not primitive to the logic, but are themselves defined using more basic assertions provided by the logic. For instance, the Hoare triple is actually defined in terms of a weakest precondition assertion. See Jung et al. [19, 20] for further details.
 
6
Iris is designed to be parametric in the choice of resources, so we can pick a particular resource for this source language and still use most of the general Iris machinery.
 
7
To be precise we ought to mention the initial states \(\sigma \) and \(\varSigma \) that https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54434-1_34/442829_1_En_34_IEq284_HTML.gif and https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54434-1_34/442829_1_En_34_IEq285_HTML.gif run in and assume they satisfy the precondition of the triple.
 
Literatur
1.
2.
Appel, A., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. TOPLAS 23(5), 657–683 (2001)CrossRef
3.
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)
4.
Birkedal, L., Bizjak, A., Schwinghammer, J.: Step-indexed relational reasoning for countable nondeterminism. Logical Methods Comput. Sci. 9(4), 1–22 (2013)MathSciNetCrossRef
5.
Birkedal, L., Støvring, K., Thamsborg, J.: The category-theoretic solution of recursive metric-space equations. Theor. Comput. Sci. 411(47), 4102–4122 (2010)MathSciNetCrossRef
6.
Brookes, S.D.: Variables as resource for shared-memory programs: semantics and soundness. Electr. Notes Theor. Comput. Sci. 158, 123–150 (2006)CrossRef
7.
Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 330–349. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-37036-6_​19CrossRefMATH
8.
9.
Craig, T.S.: Building fifo and priority-queueing spin locks from atomic swap. Technical report 93-02-02, Computer Science Department, University of Washington (1993)
10.
da 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
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.
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)
13.
Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315–327 (2009)
14.
Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010)MathSciNetCrossRef
15.
Hoffmann, J., Marmar, M., Shao, Z.: Quantitative reasoning for proving lock-freedom. In: LICS, pp. 124–133 (2013)
16.
17.
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14–26 (2001)
18.
Jones, C.B.: Tentative steps toward a development method for interfering programs. TOPLAS 5(4), 596–619 (1983)CrossRef
19.
Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: ICFP, pp. 256–269 (2016, to appear)
20.
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)
21.
Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL, pp. 205–217 (2017, to appear)
22.
Krogh-Jespersen, M., Svendsen, K., Birkedal, L.: A relational model of types-and-effects in higher-order concurrent separation logic. In: POPL, pp. 218–231 (2017, to appear)
23.
Lehmann, D., Pnueli, A., Stavi, J.: Impartiality, justice and fairness: the ethics of concurrent termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 264–277. Springer, Heidelberg (1981). doi:10.​1007/​3-540-10843-2_​22CrossRefMATH
24.
Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385–399 (2016)
25.
Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36(1), 3 (2014)CrossRef
26.
Liang, H., Feng, X., Shao, Z.: Compositional verification of termination-preserving refinement of concurrent programs. In: CSL-LICS, pp. 65:1–65:10 (2014)
27.
Magnusson, P.S., Landin, A., Hagersten, E.: Queue locks on cache coherent multiprocessors. In: International Symposium on Parallel Processing, pp. 165–171 (1994)
28.
Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290–310. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54833-8_​16CrossRefMATH
29.
30.
Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations for session-based concurrency. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 539–558. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28869-2_​27CrossRef
31.
da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P., Sutherland, J.: Modular termination verification for non-blocking concurrency. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 176–201. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49498-1_​8CrossRef
32.
33.
34.
35.
Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 350–369. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-37036-6_​20CrossRefMATH
36.
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)
37.
Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-74407-8_​18CrossRef
38.
39.
Willsey, M., Prabhu, R., Pfenning, F.: Design and implementation of concurrent C0. In: Linearity (2016)
40.
41.
Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electr. Notes Theor. Comput. Sci. 171(4), 73–93 (2007)CrossRef
Metadaten
Titel
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
verfasst von
Joseph Tassarotti
Ralf Jung
Robert Harper
Copyright-Jahr
2017
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_34