Verifying concurrent, crash-safe systems with Perennial

被引：41
作者：
Chajed, Tej [1 ]
Tassarotti, Joseph [2 ]
Kaashoek, M. Frans [1 ]
Zeldovich, Nickolai [1 ]
机构：
[1] MIT CSAIL, Cambridge, MA 02139 USA
[2] Boston Coll, Chestnut Hill, MA 02167 USA
来源：
PROCEEDINGS OF THE TWENTY-SEVENTH ACM SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES (SOSP '19) | 2019年
基金：
美国国家科学基金会;
关键词：
Concurrency; Separation Logic; Crash Safety; CORRECTNESS; REFINEMENT; LOGIC;
D O I：
10.1145/3341301.3359632
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework's proofs are machine checked.
引用
收藏
页码：243 / 258
页数：16
相关论文
共 39 条
  • [1] COMPLX: A Verification Framework for Concurrent Imperative Programs
    Amani, Sidney
    Andronick, June
    Bortin, Maksym
    Lewis, Corey
    Rizkallah, Christine
    Tuong, Joseph
    [J]. PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17, 2017, : 138 - 150
  • [2] Bizjak A., 2019, P ACM PROGRAMMING LA
  • [3] VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
    Cao, Qinxiang
    Beringer, Lennart
    Gruetter, Samuel
    Dodds, Josiah
    Appel, Andrew W.
    [J]. JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) : 367 - 422
  • [4] Chajed T, 2018, PROCEEDINGS OF THE 13TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION, P307
  • [5] Argosy: Verifying Layered Storage Systems with Recovery Refinement
    Chajed, Tej
    Tassarotti, Joseph
    Kaashoek, M. Frans
    Zeldovich, Nickolai
    [J]. PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 1054 - 1068
  • [6] Chargueraud A, 2011, ICFP 11 - PROCEEDINGS OF THE 2011 ACM SIGPLAN: INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, P418
  • [7] Using Crash Hoare Logic for Certifying the FSCQ File System
    Chen, Haogang
    Ziegler, Daniel
    Chajed, Tej
    Chlipala, Adam
    Kaashoek, M. Frans
    Zeldovich, Nickolai
    [J]. SOSP'15: PROCEEDINGS OF THE TWENTY-FIFTH ACM SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES, 2015, : 18 - 37
  • [8] Chlipala A, 2011, PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, P234
  • [9] Views: Compositional Reasoning for Concurrent Programs
    Dinsdale-Young, Thomas
    Birkedal, Lars
    Gardner, Philippa
    Parkinson, Matthew
    Yang, Hongseok
    [J]. ACM SIGPLAN NOTICES, 2013, 48 (01) : 287 - 299
  • [10] Modular, crash-safe refinement for ASMs with submachines
    Ernst, Gidon
    Pfaehler, Joerg
    Schellhorn, Gerhard
    Reif, Wolfgang
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2016, 131 : 3 - 21
1234