The examples directory contains a number of small distributed systems
that have been instrumented with DInv's interface. Using DInv is a
mulit step procedure. Each of the example programs is paired with a
script run.sh. The script oversees the execution of each stage, and
pipes each steps output into its successor. The scripts have a
standard interface
* `./run.sh` : Standard execution, results printed to standard out,
all generated files removed after execution.
+ Options :
* -d : dirty run, the generated files at each stage are
not remove after execution
* -c : cleanup generated files
Hello DInv is our introductory example program, in which a client
sends "Hello" to a server, and the server responds with the time. The execution of each
stage of DInv has been bash scripted in
DInvDirectory/examples/helloDinv/run.sh to run the example
- `cd DinvDirectory/examples/helloDinv/1
.\run.shThe inferred data invariant of this execution are the message strings passed between client and server.
Sum is a client server system. The client randomly generates values
for two variables term1 and term2 over a constant range. The terms are sent to the
server which adds them, and sends back the results as the variable
sum. Inferred invariant for this example include
server-sum = client-term1 + client-term2server-sum >= client-term2server-sum >= client-term1
Linear is a three host system. The hosts are client, coeff, and
linn. The hosts only pass messages with their neighbours ie client <--> coeff <--> linn.
Similar to the sum system the client randomly generates two terms,
packages them, and sends them to its neighbour coeff. coeff
generates a coefficient for the first term, then packages it along
with the first two terms and sends to linn. linn calculates the
linear equation linn = coeff * term1 + term2. The variables sum is
propagated back through coeff to the client host.
detected invariant include
linn > coefflinn > term1linn > term2