-
Notifications
You must be signed in to change notification settings - Fork 2
/
meta.yml
148 lines (116 loc) · 6.02 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
---
fullname: VLSM
shortname: vlsm
organization: runtimeverification
community: false
dune: false
action: true
coqdoc: true
synopsis: >-
Coq formalization of validating labelled state transition
and message production systems
description: |-
The theory of Validating Labelled State transition and Message
production systems (VLSMs) enables describing and proving properties
of distributed systems executing in the presence of faults. This
project contains a formalization of this theory in the Coq proof
assistant along with several examples of distributed protocols
modeled and verified using VLSMs, including the ELMO
(Equivocation-Limited Message Observer) family of message
validating protocols and the Paxos protocol for crash-tolerant
distributed consensus.
publications:
- pub_doi: 10.48550/arXiv.2202.12662
pub_url: https://arxiv.org/abs/2202.12662
pub_title: 'Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems'
authors:
- name: Mihai Calancea
- name: Denisa Diaconescu
- name: Wojciech Kołowski
- name: Elaine Li
- name: Brandon Moore
- name: Karl Palmskog
- name: Lucas Peña
- name: Grigore Roșu
- name: Traian Florin Șerbănuță
- name: Ioan Teodorescu
- name: Dafina Trufaș
- name: Jan Tušil
- name: Vlad Zamfir
opam-file-maintainer: palmskog@gmail.com
opam-file-version: dev
license:
fullname: BSD 3-Clause "New" or "Revised" License
identifier: BSD-3-Clause
file: LICENSE.md
supported_coq_versions:
text: 8.16 and later
opam: '{>= "8.16"}'
dependencies:
- opam:
name: coq-stdpp
version: '{>= "1.9.0"}'
description: |-
[Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.9.0 and later
- opam:
name: coq-itauto
description: |-
[Itauto](https://gitlab.inria.fr/fbesson/itauto)
- opam:
name: coq-equations
description: |-
[Coq-Equations](https://github.com/mattam82/Coq-Equations)
tested_coq_opam_versions:
- version: '8.16-ocaml-4.14-flambda'
- version: '8.17-ocaml-4.14-flambda'
- version: '8.18-ocaml-4.14-flambda'
namespace: VLSM
keywords:
- name: consensus
- name: fault tolerance
- name: distributed algorithms
- name: Paxos
categories:
- name: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems
build: |-
## Building instructions
We recommend using [opam](https://opam.ocaml.org) to install project dependencies.
Besides the basic building instructions below, we also provide a more detailed
[building guide](BUILDING.md), with special recommendations for Windows users.
To install the project dependencies via opam, do:
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.18.0 coq-stdpp.1.9.0 coq-itauto coq-equations
```
To build the project when you have all dependencies installed, do:
```shell
git clone https://github.com/runtimeverification/vlsm.git
cd vlsm
make # or make -j <number-of-cores-on-your-machine>
```
documentation: |-
## Documentation
### File organization
- [Lib](theories/Lib): Extensions to the [Coq standard library](https://coq.inria.fr/stdlib/) and [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/).
- [Core](theories/Core): Core VLSM definitions and results.
- [Examples](theories/Examples): Applications of VLSMs, including tutorials.
### Source documentation
- [latest coqdoc presentation of the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/toc.html)
- [latest Alectryon presentation of the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/alectryon/toc.html)
### VLSM tutorials
- [VLSMs that Generate Logical Formulas](theories/Examples/Tutorial/Formulas.v): construction of VLSMs corresponding to propositional logic symbols, with their composition having well-formed propositional formulas as valid messages.
- [VLSMs that Multiply](theories/Examples/Tutorial/Multiply.v): construction of VLSMs that perform arithmetic operations, with their composition having products of powers as valid messages.
- [Primes Composition of VLSMs](theories/Examples/Tutorial/PrimesComposition.v): construction of an infinite family of VLSMs that multiply and their composition based on primes.
- [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds. For additional background, see the [first](https://www.youtube.com/watch?v=lTNG4HJ7V6U) and [second](https://www.youtube.com/watch?v=1H7kAW26pOA) part of a workshop presentation on the formalization.
### VLSM application: ELMO
ELMO (Equivocation-Limited Message Observer) is a family of protocols that demonstrates gradual refinement of a specification to make it validating for increasingly more complex constraints.
- [BaseELMO](theories/Examples/ELMO/BaseELMO.v): basic definitions and results related to ELMO.
- [UMO](theories/Examples/ELMO/UMO.v): definition and properties of UMO (Unvalidating Message Observer) components and the UMO protocol.
- [MO](theories/Examples/ELMO/UMO.v): definition and properties of MO (Message Observer) components and the MO protocol.
- [ELMO](theories/Examples/ELMO/ELMO.v): definition and properties of ELMO components and the ELMO protocol.
### VLSM application: Paxos
[Paxos](https://en.wikipedia.org/wiki/Paxos_(computer_science)) is a protocol for achieving distributed consensus among network nodes in the presence of crash faults and message loss.
- [Abstract Specification of Consensus](theories/Examples/Paxos/Consensus.v): specification of consensus as a set of values that can be agreed on by nodes.
- [Specification of Consensus by Voting](theories/Examples/Paxos/Voting.v): specification of consensus where nodes agree on a value by voting.
- [A Basic Paxos Protocol](theories/Examples/Paxos/Paxos.v): specification of consensus by votes from a quorum of acceptor nodes and using a leader node for each ballot.
---