Theorems for free from separation logic specifications
| Autor: | Guilhem Jaber, Nikos Tzevelekos, Thomas Dinsdale-Young, Kasper Svendsen, Armaël Guéneau, Lars Birkedal |
|---|---|
| Přispěvatelé: | Department of Computer Science [Aarhus], Concordium [Aarhus], Aarhus University [Aarhus], Université de Nantes (UN), Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Uber [Aarhus], School of Electronic Engineering and Computer Science (EECS), Queen Mary University of London (QMUL), Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Linearizability
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Separation Logic Programming language Computer science Proof assistant Iris 020207 software engineering 0102 computer and information sciences 02 engineering and technology Separation logic computer.software_genre Program Specifications 01 natural sciences TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Safety Risk Reliability and Quality Protocol (object-oriented programming) computer Software TRACE (psycholinguistics) |
| Zdroj: | Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩ Birkedal, L, Dinsdale-Young, T, Guéneau, A, Jaber, G, Svendsen, K & Tzevelekos, N 2021, ' Theorems for free from separation logic specifications ', Proceedings of the ACM on Programming Languages, vol. 5, no. ICFP, 81 . https://doi.org/10.1145/3473586 Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩ |
| ISSN: | 2475-1421 |
| Popis: | International audience; Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuitively enforces a protocol on the trace of interactions between a client and the library. We show how to formalize this intuition and demonstrate how to derive "free theorems" about such interaction traces from abstract separation logic specifications. We present several examples of free theorems. In particular, we prove that a so-called logically atomic concurrent separation logic specification of a concurrent module operation implies that the operation is linearizable. All the results presented in this paper have been mechanized and formally proved in the Coq proof assistant using the Iris higher-order concurrent separation logic framework. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|