diff --git a/.gitignore b/.gitignore index f417c7c2b61cecda34e6b6ee2154b6c679380827..d0355a353b83b031d3e28d64a9593c27e140eb13 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,5 @@ *.cov *.lv4 + +bin/ diff --git a/Makefile.inc b/Makefile.inc deleted file mode 100644 index 35f622fde8c778aaa81a4a1ca9231e4f13de8667..0000000000000000000000000000000000000000 --- a/Makefile.inc +++ /dev/null @@ -1,39 +0,0 @@ -# -# To use this file, `include` it and define the following variables: -# DOT2LUS # dot2lus command, can include flags (eg. --clock) -# TOPOLOGY # graph file name, without the .dot extension -# SASA_ALGOS # .ml files used in sasa/lurette tests -# SASAFLAGS # flags passed in to sasa (eg. to define the daemon) -# - -.PHONY = build clean test verify - -# default rule -build: $(TOPOLOGY).lus - -clean: - rm -f *.cmxs *.cmx *.cmi *.o - rm -f $(TOPOLOGY).ml config.ml - rm -f *.rif *.seed - rm -f $(TOPOLOGY).lus - rm -f $(TOPOLOGY)_verify.lv4 - -test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus - lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" \ - -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle" - -verify: $(TOPOLOGY)_verify.lv4 - kind2 $< - -$(TOPOLOGY).lus: $(TOPOLOGY).dot - $(DOT2LUS) $< - -$(TOPOLOGY).cmxs: state.ml $(SASA_ALGOS) config.ml $(TOPOLOGY).ml - ocamlfind ocamlopt -package algo -shared $^ -o $@ - -$(TOPOLOGY).ml config.ml: $(TOPOLOGY).dot - sasa -reg $< - -$(TOPOLOGY)_verify.lv4: $(TOPOLOGY)_oracle.lus $(TOPOLOGY).lus verify.lus - lv6 $< -n verify --lustre-v4 -o $@ - sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@ diff --git a/README.md b/README.md index 4a69c9bf6720d03f10424a4a7378f9ae4af8f641..dfbf4bba404f0483a6c364a3ef80b06b77f49dc4 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,71 @@ -# Self-stabilizing Algorithms in LUsTre +# SALut - Self-stabilizing Algorithms in LUsTre -```shell -$ cd $example_folder -$ make build -$ make test # requires lurette and sasa algorithm -$ make verify # requires kind2 +[SALut](.) is a companion project to [Verimag's Synchrone Reactive Toolbox](https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/). + +It is dedicated to the [Simulation and Formal Verification of Self-stabilizing Algorithms](https://ensiwiki.ensimag.fr/index.php?title=IRL_-_Simulation_and_Formal_Verification_of_Self-stabilizing_Algorithms) in the [the Lustre Programming Language](https://www-verimag.imag.fr/The-Lustre-Programming-Language-and), relying on [Lurette][lurette] and [SASA](https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/) for testing/simulation and on [Kind2][kind2] for SMT-powered verification. + + +## [dot2lus](dot2lus.ml) + +### Summary + +dot2lus compiles a graph described in the [DOT format](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) into a Lustre program that executes some [Distributed Self-Stabilizing Algorithm](https://www-verimag.imag.fr/New-Book-Introduction-to-Distributed.html) over an equivalent network topology. + +``` +dot2lus <dotfile> [-o lusfile] [--clock] [--help] + -o Set output file (default is inferred from input file) + --clock Generate clocked code (default is unclocked) + --help Display this list of options ``` + +### Algorithm API + +Following the conventions used in [SASA's API](https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/algo/Algo/index.html), every algorithm currently needs to provide the following definitions, which are shared by all nodes: + +```ocaml +(* Represents a node's state. *) +type state; + +(* Enumerates the possible atomic actions a node might execute. *) +type action; +const actions_number : int; + +(* Given an integer in [0,actions_number), maps to an equivalent action. *) +function action_of_int(i : int) returns (a : action); +``` + +And each algorithmic node needs `enable` and `step` functions prefixed by its name: + +```ocaml +(* p.lus *) + +(* Computes the set of actions enabled in this configuration of current and visible neighboring nodes' state. *) +function p_enable<<const degree:int>>(this : state; neighbors : state^degree) +returns (enabled : bool^actions_number); + +(* Executes the given action, returning the updated node state. *) +function p_step<<const degree:int>>(this : state; neighbors : state^degree; action : action) +returns (new : state); +``` + +**Check out the generated Lustre topology for the graph constants it defines.** + +### Examples + +Some [example algorithms](test/) are provided in this repository. +Each folder contains a distributed algorithm defined in both OCaml+SASA and LustreV6+SALUT and with a common network topology. + +The [shared Makefile](test/Makefile.inc) has instructions on how to `build` the Lustre-defined network and use [Lurette][lurette] to `test` it agains the SASA model. + +You can also `verify` it with [Kind2][kind2]. +Note that this currently requires converting LustreV6 to LustreV4 and adding Kind2's required annotations (to the generated LV4), which is also handled by the makefile. + +### Build instructions + +```sh +$ cd src/ +$ make # => bin/dot2lus +``` + +[lurette]: https://www-verimag.imag.fr/Lurette-107.html +[kind2]: https://kind2-mc.github.io/kind2/ diff --git a/coloring/Makefile b/coloring/Makefile deleted file mode 100644 index a56bf654e425625c0a2d2dff7eadf2a58aadda6e..0000000000000000000000000000000000000000 --- a/coloring/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -DOT2LUS := ocaml ../dot2lus.ml -TOPOLOGY := dice5 -SASA_ALGOS := p.ml -SASAFLAGS := --locally-central-daemon - -include ../Makefile.inc diff --git a/bitset.lus b/lib/bitset.lus similarity index 100% rename from bitset.lus rename to lib/bitset.lus diff --git a/sas.lus b/lib/sas.lus similarity index 72% rename from sas.lus rename to lib/sas.lus index 79bffb098e66d5f6486ee7f7ac18763987d78713..f36bb3f874cf6fac8460bae0520d7459c3003199 100644 --- a/sas.lus +++ b/lib/sas.lus @@ -5,19 +5,19 @@ include "bitset.lus" function silent<<const an:int; const pn:int>>(enab: bool^an^pn) returns (y : bool); let - y = none<<pn>>(map<<any<<an>>, pn>>(enab)); + y = boolnone<<pn>>(map<<boolany<<an>>, pn>>(enab)); tel; node node_is_proper<<const an:int>>(acti, enab : bool^an) returns (y : bool); let - y = true -> all<<an>>(map<<=>,an>>(acti, pre(enab))); + y = true -> boolall<<an>>(map<<=>,an>>(acti, pre(enab))); tel; -- Any activation Ai implies Ei was previously enabled. node daemon_is_proper<<const an:int; const pn:int>>(acti, enab : bool^an^pn) returns (y : bool); let - y = all<<pn>>(map<<node_is_proper,pn>>(acti, enab)); + y = boolall<<pn>>(map<<node_is_proper,pn>>(acti, enab)); tel; -- |A| >= 1 for non-silent states. @@ -25,7 +25,7 @@ function daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^a returns (y : bool); let y = silent<<an,pn>>(enab) or - boolred<<1,pn,pn>>(map<<any<<an>>, pn>>(acti)); + boolred<<1,pn,pn>>(map<<boolany<<an>>, pn>>(acti)); tel; -- No two neighboring nodes are active at once. @@ -39,11 +39,11 @@ var no_active_adjacencies : bool ^ pn; locally_central : bool ^ pn; let - active = map<<any<<an>>, pn>>(acti); + active = map<<boolany<<an>>, pn>>(acti); active_adjacencies = map<<inter,pn>>(active^pn, adjacency); - no_active_adjacencies = map<<none<<pn>>, pn>>(active_adjacencies); + no_active_adjacencies = map<<boolnone<<pn>>, pn>>(active_adjacencies); locally_central = map<<=>,pn>>(active, no_active_adjacencies); - y = all<<pn>>(locally_central); + y = boolall<<pn>>(locally_central); tel; -- |A| = 1 for non-silent states. @@ -51,7 +51,7 @@ function daemon_is_central<<const an:int; const pn:int>>(acti : bool^an^pn) returns (y : bool); let y = silent<<an,pn>>(enab) or - boolred<<1,1,pn>>(map<<any<<an>>, pn>>(acti)); + boolred<<1,1,pn>>(map<<boolany<<an>>, pn>>(acti)); tel; -- |A| = n for non-silent states. @@ -59,12 +59,12 @@ function daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^a returns (y:bool); let y = silent<<an,pn>>(enab) or - boolred<<pn,pn,pn>>(map<<any<<an>>, pn>>(acti)); + boolred<<pn,pn,pn>>(map<<boolany<<an>>, pn>>(acti)); tel; -- Measures time complexity in moves. node move_count<<const an:int; const pn:int>>(acti : bool^an^pn) returns (count:int); let - count = (0 -> pre(count)) + pop_count<<pn>>(map<<any<<an>>, pn>>(acti)); + count = (0 -> pre(count)) + pop_count<<pn>>(map<<boolany<<an>>, pn>>(acti)); tel; diff --git a/utils.lus b/lib/utils.lus similarity index 77% rename from utils.lus rename to lib/utils.lus index 289a88773eebfcbaf9845083ff1e241008d27d1a..b17500d3585a19e495884636cde9f741f0404f2c 100644 --- a/utils.lus +++ b/lib/utils.lus @@ -4,7 +4,7 @@ let r = with (N = 1) then [ 0 ] else range<<N-1>>() | [ N-1 ]; tel; --- "First-class" if statement, since we don't have lambdas. +-- First-class if statement, since we don't have lambdas. function choice_of_bool<<type T; const t:T; const f:T>>(b : bool) returns (y : T); let y = if b then t else f; @@ -13,17 +13,17 @@ tel; -- |> true -> 1 | false -> 0 function int_of_bool = choice_of_bool<<int, 1, 0>>; -function none<<const N:int>>(s : bool^N) returns (y : bool); +function boolnone<<const N:int>>(s : bool^N) returns (y : bool); let y = boolred<<0,0,N>>(s); tel; -function any<<const N:int>>(s : bool^N) returns (y : bool); +function boolany<<const N:int>>(s : bool^N) returns (y : bool); let y = boolred<<1,N,N>>(s); tel; -function all<<const N:int>>(s : bool^N) returns (y : bool); +function boolall<<const N:int>>(s : bool^N) returns (y : bool); let y = boolred<<N,N,N>>(s); tel; diff --git a/src/Makefile b/src/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..48de5aba557a2554a14562abe835a70e84e1de47 --- /dev/null +++ b/src/Makefile @@ -0,0 +1,13 @@ +.PHONY = build clean + +# default rule +build: ../bin/dot2lus + +clean: + rm -f *.cmx *.cmi *.o + rm -f ../bin/dot2lus + -rmdir ../bin + +../bin/dot2lus: dot2lus.ml + mkdir -p ../bin + ocamlfind ocamlopt -o ../bin/$@ -linkpkg -package sasacore $^ diff --git a/dot2lus.ml b/src/dot2lus.ml similarity index 98% rename from dot2lus.ml rename to src/dot2lus.ml index dc11fde7f4864ca06062a72558559245e7d60d34..0d70f1911c6bae18a9bd55d3fa5e0a656b3dd885 100644 --- a/dot2lus.ml +++ b/src/dot2lus.ml @@ -1,5 +1,5 @@ -#use "topfind";; -#require "sasacore";; (* simplified DOT parsing *) +(* #use "topfind";; *) +(* #require "sasacore";; *) open Sasacore diff --git a/test/Makefile.inc b/test/Makefile.inc new file mode 100644 index 0000000000000000000000000000000000000000..346050d0c17913148375619dab19250ce2f48075 --- /dev/null +++ b/test/Makefile.inc @@ -0,0 +1,44 @@ +# +# To use this file, define the following variables and `include` it: +# TOPOLOGY # graph file name, without the .dot extension +# DOT2LUSFLAGS # optional: dot2lus flags (eg. --clock) +# SASA_ALGOS # .ml files used in sasa/lurette tests +# SASAFLAGS # optional: flags passed in to sasa (eg. to define the daemon) +# + +.PHONY = build all clean test verify + +# extra ../ because this is called from within each test folder +D2L := ../../bin/dot2lus + +# default rule +build: $(TOPOLOGY).lus + +all: $(TOPOLOGY).lus $(TOPOLOGY).cmxs $(TOPOLOGY)_verify.lv4 + +clean: + rm -f *.cmxs *.cmx *.cmi *.o + rm -f $(TOPOLOGY).ml config.ml + rm -f *.rif *.seed + rm -f $(TOPOLOGY).lus + rm -f $(TOPOLOGY)_verify.lv4 + +test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus + lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle" + +verify: $(TOPOLOGY)_verify.lv4 + kind2 $< + +$(TOPOLOGY).lus: $(TOPOLOGY).dot + $(D2L) $(DOT2LUSFLAGS) $< + +$(TOPOLOGY).cmxs: state.ml $(SASA_ALGOS) config.ml $(TOPOLOGY).ml + ocamlfind ocamlopt -package algo -shared $^ -o $@ + +$(TOPOLOGY).ml config.ml: $(TOPOLOGY).dot + sasa -reg $< + +# XXX: this method of adding kind2 annotations is brittle +$(TOPOLOGY)_verify.lv4: $(TOPOLOGY)_oracle.lus $(TOPOLOGY).lus verify.lus + lv6 $< -n verify --lustre-v4 -o $@ + sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@ diff --git a/test/coloring/Makefile b/test/coloring/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..e6bc54cd3d0299779ed66b44ed12ca7ac6917a15 --- /dev/null +++ b/test/coloring/Makefile @@ -0,0 +1,6 @@ +TOPOLOGY ?= dice5 +DOT2LUSFLAGS ?= +SASA_ALGOS := p.ml +SASAFLAGS += --locally-central-daemon + +include ../Makefile.inc diff --git a/coloring/dice5.dot b/test/coloring/dice5.dot similarity index 100% rename from coloring/dice5.dot rename to test/coloring/dice5.dot diff --git a/coloring/dice5_oracle.lus b/test/coloring/dice5_oracle.lus similarity index 100% rename from coloring/dice5_oracle.lus rename to test/coloring/dice5_oracle.lus diff --git a/coloring/p.lus b/test/coloring/p.lus similarity index 95% rename from coloring/p.lus rename to test/coloring/p.lus index 398e2852bd18576118d446c5a2dd5dda9af6fb59..94e10a33c15db1343aa958c0c85b222384d19d7d 100644 --- a/coloring/p.lus +++ b/test/coloring/p.lus @@ -1,4 +1,4 @@ -include "../bitset.lus" +include "../../lib/bitset.lus" type state = int; diff --git a/coloring/p.ml b/test/coloring/p.ml similarity index 100% rename from coloring/p.ml rename to test/coloring/p.ml diff --git a/coloring/state.ml b/test/coloring/state.ml similarity index 100% rename from coloring/state.ml rename to test/coloring/state.ml diff --git a/coloring/verify.lus b/test/coloring/verify.lus similarity index 96% rename from coloring/verify.lus rename to test/coloring/verify.lus index c9e6a67d9dae21ef3b590c92024910dd069e258d..957a20cbedc0bb2cfda5f2db0d4ec99c98e09a3a 100644 --- a/coloring/verify.lus +++ b/test/coloring/verify.lus @@ -1,4 +1,4 @@ -include "../sas.lus" +include "../../lib/sas.lus" node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool); var diff --git a/test/token/Makefile b/test/token/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..ee04475bd0d92c08787dcfba933bb7f84bdbfd32 --- /dev/null +++ b/test/token/Makefile @@ -0,0 +1,5 @@ +TOPOLOGY ?= ring8 +DOT2LUSFLAGS ?= +SASA_ALGOS := p.ml root.ml + +include ../Makefile.inc diff --git a/token/p.lus b/test/token/p.lus similarity index 100% rename from token/p.lus rename to test/token/p.lus diff --git a/token/p.ml b/test/token/p.ml similarity index 100% rename from token/p.ml rename to test/token/p.ml diff --git a/token/ring3.dot b/test/token/ring3.dot similarity index 100% rename from token/ring3.dot rename to test/token/ring3.dot diff --git a/token/ring3_oracle.lus b/test/token/ring3_oracle.lus similarity index 100% rename from token/ring3_oracle.lus rename to test/token/ring3_oracle.lus diff --git a/token/ring8.dot b/test/token/ring8.dot similarity index 100% rename from token/ring8.dot rename to test/token/ring8.dot diff --git a/token/ring8_oracle.lus b/test/token/ring8_oracle.lus similarity index 100% rename from token/ring8_oracle.lus rename to test/token/ring8_oracle.lus diff --git a/token/root.lus b/test/token/root.lus similarity index 100% rename from token/root.lus rename to test/token/root.lus diff --git a/token/root.ml b/test/token/root.ml similarity index 100% rename from token/root.ml rename to test/token/root.ml diff --git a/token/state.ml b/test/token/state.ml similarity index 100% rename from token/state.ml rename to test/token/state.ml diff --git a/token/verify.lus b/test/token/verify.lus similarity index 86% rename from token/verify.lus rename to test/token/verify.lus index 49ec2000f273d78dbf661b305260ead271e419cb..568edda70d26f1bfdecebdb702c02f110d9c317b 100644 --- a/token/verify.lus +++ b/test/token/verify.lus @@ -1,5 +1,5 @@ -include "../sas.lus" -include "../utils.lus" +include "../../lib/sas.lus" +include "../../lib/utils.lus" node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool); var @@ -15,7 +15,7 @@ let nodes, enables = topology(activations, inits); -- a node "has the token" when it is enabled - tokens = pop_count<<card>>(map<<any<<actions_number>>, card>>(enables)); + tokens = pop_count<<card>>(map<<boolany<<actions_number>>, card>>(enables)); -- stability in this algo means mutual exclusion: 1 node enabled at a time legitimate = tokens = 1; diff --git a/token/Makefile b/token/Makefile deleted file mode 100644 index 59deaa5e3f13a3393034126e0f35d436936523f8..0000000000000000000000000000000000000000 --- a/token/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -DOT2LUS := ocaml ../dot2lus.ml -TOPOLOGY := ring8 -SASA_ALGOS := p.ml root.ml -SASAFLAGS := --distributed-daemon - -include ../Makefile.inc