دورية أكاديمية
Cosmo: A Concurrent Separation Logic for Multicore OCaml
| العنوان: | Cosmo: A Concurrent Separation Logic for Multicore OCaml |
|---|---|
| المؤلفون: | Mével, Glen, Jourdan, Jacques-Henri, Pottier, François |
| المساهمون: | Université Paris-Saclay, Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS), ACM |
| المصدر: | ISSN: 2475-1421 ; Proceedings of the ACM on Programming Languages ; ICFP 2020 - 25th ACM SIGPLAN International Conference on Functional Programming ; https://hal.science/hal-02929998Test ; Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), ⟨10.1145/3408978⟩ ; https://icfp20.sigplan.orgTest/. |
| بيانات النشر: | HAL CCSD ACM |
| سنة النشر: | 2020 |
| المجموعة: | Université de Rennes 1: Publications scientifiques (HAL) |
| مصطلحات موضوعية: | Separation logic, Program verification, Concurrency, Weak memory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
| جغرافية الموضوع: | New-York / Virtual, United States |
| الوصف: | International audience ; Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronization can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model. |
| نوع الوثيقة: | article in journal/newspaper |
| اللغة: | English |
| العلاقة: | hal-02929998; https://hal.science/hal-02929998Test; https://hal.science/hal-02929998/documentTest; https://hal.science/hal-02929998/file/mevel2020cosmo.pdfTest |
| DOI: | 10.1145/3408978 |
| الإتاحة: | https://doi.org/10.1145/3408978Test https://hal.science/hal-02929998Test https://hal.science/hal-02929998/documentTest https://hal.science/hal-02929998/file/mevel2020cosmo.pdfTest |
| حقوق: | info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.B88AB81C |
| قاعدة البيانات: | BASE |
| DOI: | 10.1145/3408978 |
|---|