Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Morten Krogh-Jespersen; Amin Timany; Marit Edna Ohlenbusch; Simon Oddershede Gregersen; Lars Birkedal

doi:10.1007/978-3-030-44914-8_13

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Morten Krogh-Jespersen
, Amin Timany
, Marit Edna Ohlenbusch
, Simon Oddershede Gregersen^*
, Lars Birkedal

^*Corresponding author for this work

Department of Computer Science

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

26 Citations (Scopus)

68 Downloads (Pure)

Abstract

Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.

Original language	English
Title of host publication	Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
Editors	Peter Müller
Number of pages	30
Publisher	Springer
Publication date	1 Jan 2020
Pages	336-365
ISBN (Print)	9783030449131
DOIs	https://doi.org/10.1007/978-3-030-44914-8_13
Publication status	Published - 1 Jan 2020
Event	29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020

Conference

Conference	29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/2020 → 30/04/2020

Series	Lecture Notes in Computer Science
Volume	12075
ISSN	0302-9743

Keywords

Concurrency
Distributed systems
Formal verification
Higher-order logic
Separation logic

Access to Document

10.1007/978-3-030-44914-8_13Licence: CC BY

Krogh-Jespersen2020_Chapter_AnerisAMechanisedLogicForModulFinal published version, 513 KBLicence: CC BY

Library access?

Check availability with the Royal Danish Library

Cite this

Krogh-Jespersen, M., Timany, A., Ohlenbusch, M. E., Gregersen, S. O., & Birkedal, L. (2020). Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In P. Müller (Ed.), Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 336-365). Springer. https://doi.org/10.1007/978-3-030-44914-8_13

Krogh-Jespersen, Morten ; Timany, Amin ; Ohlenbusch, Marit Edna et al. / Aneris : A Mechanised Logic for Modular Reasoning about Distributed Systems. Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. editor / Peter Müller. Springer, 2020. pp. 336-365 (Lecture Notes in Computer Science, Vol. 12075).

@inproceedings{d0fae9bfb96247558822a9baf1f715ec,

title = "Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems",

abstract = "Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.",

keywords = "Concurrency, Distributed systems, Formal verification, Higher-order logic, Separation logic",

author = "Morten Krogh-Jespersen and Amin Timany and Ohlenbusch, \{Marit Edna\} and Gregersen, \{Simon Oddershede\} and Lars Birkedal",

year = "2020",

month = jan,

day = "1",

doi = "10.1007/978-3-030-44914-8\_13",

language = "English",

isbn = "9783030449131",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "336--365",

editor = "Peter M{\"u}ller",

booktitle = "Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings",

address = "Netherlands",

note = "29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

}

Krogh-Jespersen, M, Timany, A, Ohlenbusch, ME, Gregersen, SO & Birkedal, L 2020, Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. in P Müller (ed.), Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Springer, Lecture Notes in Computer Science, vol. 12075, pp. 336-365, 29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25/04/2020. https://doi.org/10.1007/978-3-030-44914-8_13

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. / Krogh-Jespersen, Morten; Timany, Amin; Ohlenbusch, Marit Edna et al.
Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. ed. / Peter Müller. Springer, 2020. p. 336-365 (Lecture Notes in Computer Science, Vol. 12075).

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Aneris

T2 - 29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

AU - Krogh-Jespersen, Morten

AU - Timany, Amin

AU - Ohlenbusch, Marit Edna

AU - Gregersen, Simon Oddershede

AU - Birkedal, Lars

PY - 2020/1/1

Y1 - 2020/1/1

N2 - Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.

AB - Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.

KW - Concurrency

KW - Distributed systems

KW - Formal verification

KW - Higher-order logic

KW - Separation logic

UR - https://www.scopus.com/pages/publications/85084006085

U2 - 10.1007/978-3-030-44914-8_13

DO - 10.1007/978-3-030-44914-8_13

M3 - Article in proceedings

AN - SCOPUS:85084006085

SN - 9783030449131

T3 - Lecture Notes in Computer Science

SP - 336

EP - 365

BT - Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings

A2 - Müller, Peter

PB - Springer

Y2 - 25 April 2020 through 30 April 2020

ER -

Krogh-Jespersen M, Timany A, Ohlenbusch ME, Gregersen SO, Birkedal L. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In Müller P, editor, Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Springer. 2020. p. 336-365. (Lecture Notes in Computer Science, Vol. 12075). doi: 10.1007/978-3-030-44914-8_13

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Abstract

Conference

Keywords

Access to Document

Library access?

Other files and links

Fingerprint

Cite this