GitLab

Relatively small model batch.
These models are used to test the implementation of the distributed Union-Find.

* benchmarks/models/*.txt: here.

* benchmarks/results/README: here.

Each sending depends on the depth.
Only one thread per machine manages the reception of messages.
This test was performed with 3 machines.

* benchmarks/results/central3_depth/*: here.

Each sending depends on the depth.
The algorithm uses a second DFS to close the successors.
Only one thread per machine manages the reception of messages.
This test was performed with 2 machines.

* benchmarks/results/central2_depth_dfs/*: here.

Each sending depends on the depth.
Only one thread per machine manages the reception of messages.
This test was performed with 2 machines.

* benchmarks/results/central2_depth/*: here.

Each sending depends on the depth.
The algorithm uses a second DFS to close the successors.

* benchmarks/results/depth_dfs/*: here.

Each shipment depends directly on the threshold.

* benchmarks/results/pop_end/*: here.

Each shipment depends directly on the threshold.
The algorithm uses a second DFS to close the successors.

* benchmarks/results/pop_dfs/*: here.

Each shipment depends directly on the threshold.
The algorithm uses a second DFS to close the successors.

* benchmarks/results/pop_dfs_end/*: here.

* benchmarks/results/depth_end/README: here.

Each sending depends on the depth.

* benchmarks/results/*: here.

* benchmarks/scripts/README: here.

* benchmarks/scripts/dve_to_dve2c.sh: here.

Relatively small model batch.
These models are used to test the implementation of the distributed DFS,
and must be compiled beforehand with the script dve_to_dve2c.

* benchmarks/models/*: here.

This report is divided into three parts:
The first is a set of definitions related to model checking,
the second deals with deadlock verification and the implementation of a
distributed DFS and finally, the third part deals with the distributed
Union-Find structure.

* report/1808.pdf,
report/slides.pdf: here.