|
| 1 | +<!--- |
| 2 | +This file was generated from `meta.yml`, please do not edit manually. |
| 3 | +Follow the instructions on https://github.com/coq-community/templates to regenerate. |
| 4 | +---> |
1 | 5 | # Disel: Distributed Separation Logic |
2 | 6 |
|
3 | | -Implementation and case studies of Disel, a separation-style logic for |
4 | | -compositional verification of distributed systems. |
| 7 | +[![Docker CI][docker-action-shield]][docker-action-link] |
5 | 8 |
|
6 | | -This code accompanies the paper entitled [Programming and Proving with Distributed Protocols](http://homes.cs.washington.edu/~jrw12/disel.pdf) |
7 | | -by Ilya Sergey, James R. Wilcox, and Zachary Tatlock, in the POPL 2018 proceedings. |
| 9 | +[docker-action-shield]: https://github.com/DistributedComponents/disel/workflows/Docker%20CI/badge.svg?branch=master |
| 10 | +[docker-action-link]: https://github.com/DistributedComponents/disel/actions?query=workflow:"Docker%20CI" |
8 | 11 |
|
9 | | -## Building the Project |
10 | 12 |
|
11 | | -### Requirements |
12 | 13 |
|
13 | | -* [Coq 8.11 or later](https://coq.inria.fr) |
14 | | -* [Mathematical Components 1.10.0 or later](http://math-comp.github.io/math-comp/) (`ssreflect` suffices) |
15 | | -* [FCSL PCM library 1.3.0 or later](https://github.com/imdea-software/fcsl-pcm) |
16 | | -* [OCaml 4.05.0 or later](https://ocaml.org) (to compile and run the extracted applications) |
17 | 14 |
|
18 | | -### Building Manually |
| 15 | +Disel is a framework for implementation and compositional verification of |
| 16 | +distributed systems and their clients in Coq. In Disel, users implement |
| 17 | +distributed systems using a domain specific language shallowly embedded in Coq |
| 18 | +which provides both high-level programming constructs as well as low-level |
| 19 | +communication primitives. Components of composite systems are specified in Disel |
| 20 | +as protocols, which capture system-specific logic and disentangle system definitions |
| 21 | +from implementation details. |
19 | 22 |
|
20 | | -If Coq is not installed such that its binaries like `coqc` and |
21 | | -`coq_makefile` are in the `PATH`, then the `COQBIN` environment variable |
22 | | -must be set to point to the directory containing such binaries. For |
23 | | -example: |
24 | | -``` |
25 | | -export COQBIN=/home/user/coq/bin/ |
26 | | -``` |
27 | | - |
28 | | -To build the whole project, including examples, simply run `make` |
29 | | -in the root directory of the repository. For a faster build, use |
30 | | -several parallel make jobs, e.g., `make -j 4`. |
| 23 | +## Meta |
31 | 24 |
|
32 | | -### Installation via OPAM |
| 25 | +- Author(s): |
| 26 | + - Ilya Sergey (initial) |
| 27 | + - James R. Wilcox (initial) |
| 28 | +- License: [BSD 2-Clause "Simplified" license](LICENSE) |
| 29 | +- Compatible Coq versions: 8.14 or later |
| 30 | +- Additional dependencies: |
| 31 | + - [MathComp](https://math-comp.github.io) 1.13.0 or later (`ssreflect` suffices) |
| 32 | + - [FCSL PCM](https://github.com/imdea-software/fcsl-pcm) 1.7.0 or later |
| 33 | +- Coq namespace: `DiSeL` |
| 34 | +- Related publication(s): |
| 35 | + - [Programming and Proving with Distributed Protocols](http://jamesrwilcox.com/disel.pdf) doi:[10.1145/3158116](https://doi.org/10.1145/3158116) |
33 | 36 |
|
34 | | -The latest release of the framework components of the project may be installed into Coq's |
35 | | -`user-contrib` directory via [OPAM](https://opam.ocaml.org/doc/Install.html) |
36 | | -for easy use in other developments; this will automatically install all |
37 | | -requirements. |
| 37 | +## Building and installation instructions |
38 | 38 |
|
39 | | -Make sure OPAM is installed and use the following commands: |
| 39 | +The easiest way to install the latest released version of Disel: Distributed Separation Logic |
| 40 | +is via [OPAM](https://opam.ocaml.org/doc/Install.html): |
40 | 41 |
|
41 | | -``` |
| 42 | +```shell |
42 | 43 | opam repo add coq-released https://coq.inria.fr/opam/released |
43 | 44 | opam install coq-disel |
44 | 45 | ``` |
45 | 46 |
|
46 | | -As an alternative, a VM for a previous version has been provided for |
47 | | -your convenience and is described below. |
| 47 | +To instead build and install manually, do: |
48 | 48 |
|
49 | | -## Project Structure |
| 49 | +``` shell |
| 50 | +git clone https://github.com/DistributedComponents/disel.git |
| 51 | +cd disel |
| 52 | +make # or make -j <number-of-cores-on-your-machine> |
| 53 | +make install |
| 54 | +``` |
50 | 55 |
|
51 | | -* `Core` -- Disel implementation, metatheory and inference rules; |
52 | 56 |
|
53 | | -* `Examples` -- Case studies implemented in Disel |
| 57 | +## Project Structure |
54 | 58 |
|
| 59 | +- `Core` -- Disel implementation, metatheory and inference rules; |
| 60 | +- `Examples` -- Case studies implemented in Disel |
55 | 61 | - `Calculator` -- the calculator system; |
56 | | - |
57 | 62 | - `Greeter` -- a toy "Hello World"-like protocol, where |
58 | 63 | participants can only exchange greetings with each other; |
59 | | - |
60 | 64 | - `TwoPhaseCommit` -- Two Phase Commit protocol implementation; |
61 | | - |
62 | 65 | - `Query` -- querying protocol and its composition with Two Phase |
63 | 66 | Commit via hooks; |
64 | | - |
65 | | -* `shims` -- DiSeL runtime system |
| 67 | +- `shims` -- DiSeL runtime system |
66 | 68 |
|
67 | 69 | ## VM Instructions |
68 | 70 |
|
|
0 commit comments