зеркало из https://github.com/microsoft/ivy.git
workaround for Jekyll relative path bug
This commit is contained in:
Ken McMillan
Родитель
e013e5de77
Коммит
3cba8168fe
|
|
@ -109,16 +109,16 @@ This produces the following rather uninformative display:
|
|||
Let's ask IVy to check our invariant. We select the `Check induction`
|
||||
operation, like this:
|
||||
|
||||
|
||||
<p><img src="images/client_server2.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Here's what IVy says:
|
||||
|
||||
|
||||
<p><img src="images/client_server8.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
It is telling us that our conjectured invariant fails the consecution test.
|
||||
When we click OK, we see the counter-example to induction:
|
||||
|
||||
|
||||
<p><img src="images/client_server9.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
On the left-hand side of the display, we see a transition of the
|
||||
program from a state labeled `0` to a state labeled `1`. The action
|
||||
|
|
@ -144,7 +144,7 @@ display further information about the state.
|
|||
Checking the box to view the `semaphore`
|
||||
relation, we observe the following:
|
||||
|
||||
|
||||
<p><img src="images/client_server10.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Notice that the `server` node is now labeled with `semaphore`, meaning
|
||||
that `semaphore` is true for this node (if it were false, the label would
|
||||
|
|
@ -153,7 +153,7 @@ the semaphore should be down. We will conjecture that in fact
|
|||
this 'bad pattern' never occurs. To do this we select the `Gather` option
|
||||
from the `Conjecture` menu. When then see the following:
|
||||
|
||||
|
||||
<p><img src="images/client_server11.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
IVy has collect three facts about the displayed state, shown under the
|
||||
heading 'Constraints'. These facts are a logical representation of the
|
||||
|
|
@ -168,7 +168,7 @@ generalize it to produce new conjectured invariant about the program
|
|||
state. Choosing the `Strengthen` option from the `Conjecture` menu, we
|
||||
see:
|
||||
|
||||
|
||||
<p><img src="images/client_server12.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
IVy is suggesting to add this fact to the list of conjectured invariants:
|
||||
|
||||
|
|
@ -181,13 +181,13 @@ conjectured invariants.
|
|||
We can now try checking inductiveness again with our new conjecture.
|
||||
We see the following:
|
||||
|
||||
|
||||
<p><img src="images/client_server13.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
We now have a proof that our program is safe. Of course, we want to
|
||||
save that proof so we can use it again later. We select `Save invariant` from
|
||||
the `File` menu and enter a file name:
|
||||
|
||||
|
||||
<p><img src="images/client_server14.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Here is the content of the file:
|
||||
|
||||
|
|
@ -217,7 +217,7 @@ There are several ways in which we can get some automated help with
|
|||
this task. Let's go back to the counterexample in which one client is
|
||||
connected, but the semaphore is up:
|
||||
|
||||
|
||||
<p><img src="images/client_server11.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This pattern actually contains an irrelevant fact. That is, our bad
|
||||
pattern requires that there are two distinct nodes, `0` and `1`. In
|
||||
|
|
@ -229,11 +229,11 @@ that is, `semaphore(0)` and `link(0,0)`.
|
|||
To check this idea, we remove the irrelevant fact from the pattern by clicking on it.
|
||||
The unwanted fact becomes gray:
|
||||
|
||||
|
||||
<p><img src="images/client_server15.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
When we strengthen using this pattern, we get this:
|
||||
|
||||
|
||||
<p><img src="images/client_server16.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
That is, our new conjecture says that no client can be connected to a
|
||||
server with the semaphore up, but it doesn't depend on the existence
|
||||
|
|
@ -253,7 +253,7 @@ unwanted facts, we can select `Minimize` from the `Conjecture`
|
|||
menu. IVy ask for the number of steps to check. Somewhat arbitrarily,
|
||||
we choose four. This is the result we get:
|
||||
|
||||
|
||||
<p><img src="images/client_server17.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
IVy has recognized that there is a more general pattern that can be
|
||||
ruled out if we consider only four steps of execution of the protocol.
|
||||
|
|
@ -276,7 +276,7 @@ occur within some fixed number of steps.
|
|||
|
||||
To see how this goes, suppose we get into this situation:
|
||||
|
||||
|
||||
<p><img src="images/client_server18.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Here, we didn't consider the semaphore and we conjectured a bad
|
||||
pattern in which there is a client connected to a server. Obviously
|
||||
|
|
@ -284,13 +284,13 @@ pattern in which there is a client connected to a server. Obviously
|
|||
we can select `Bounded check` from the `Conjecture` menu. Here's what we see when we choose
|
||||
one step:
|
||||
|
||||
|
||||
<p><img src="images/client_server19.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
|
||||
IVy tried the conjecture that node client is connected to any server
|
||||
for one step and found it false. If we click `View`, here is what we see:
|
||||
|
||||
|
||||
<p><img src="images/client_server20.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
IVy has created a new tab in the interface with a trace consisting of
|
||||
two steps. The arrow represents a transition from state `0` to state
|
||||
|
|
@ -298,7 +298,7 @@ two steps. The arrow represents a transition from state `0` to state
|
|||
Clicking on state `0`, and checking the `link` and `semaphore` relations,
|
||||
we see the following:
|
||||
|
||||
|
||||
<p><img src="images/client_server21.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
That is, in the initial state there are two clients and one server, the
|
||||
semaphore of the server is up and there are no links.
|
||||
|
|
@ -306,7 +306,7 @@ semaphore of the server is up and there are no links.
|
|||
Now, clicking on state `1`, we see our proposed bad pattern. This
|
||||
means that the pattern can actually occur.
|
||||
|
||||
|
||||
<p><img src="images/client_server22.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
# Debugging
|
||||
|
||||
|
|
@ -315,25 +315,25 @@ To see details of the execution path, we left-click on the action
|
|||
actions. In this case, we see that the environment has decided to call
|
||||
the exported action `connect`:
|
||||
|
||||
|
||||
<p><img src="images/client_server23.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Applying `Decompose` to this action we see:
|
||||
|
||||
|
||||
<p><img src="images/client_server24.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This shows us that `connect` is made up of a sequence of three smaller
|
||||
actions. If we left-click on one of these and choose `Show source`,
|
||||
the corresponding source line is display. By single-clicking on a state,
|
||||
we can display it graphically:
|
||||
|
||||
|
||||
<p><img src="images/client_server25.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This is state 2, which is after the link is created, but before the
|
||||
semaphore is lowered. The two identifiers `fml:x` and `fml:y` represent
|
||||
the formal parameters of action `connect`. We can see which client is `x`
|
||||
at this point in the code by checking the `+` box for `fml:x`:
|
||||
|
||||
|
||||
<p><img src="images/client_server26.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
As we decompose actions, we build up a sequence of tabs,
|
||||
corresponding to something like a stack trace of the program's
|
||||
|
|
@ -351,7 +351,7 @@ strengthen the invariant with a conjecture that isn't true. If this happens,
|
|||
or if we regret a conjecture for any other reason, we can remove it using
|
||||
the `Weaken` operation in the `Invariant` menu:
|
||||
|
||||
|
||||
<p><img src="images/client_server27.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This dialog can be resized to see long formulas.
|
||||
|
||||
|
|
|
|||
|
|
@ -341,11 +341,11 @@ method](client_server_example.html). We start IVy using this command:
|
|||
We start, as usual, with `Invariant|Check induction`. Ivy tells us the
|
||||
the safety check failed, meaning that an assert fails in some action:
|
||||
|
||||
|
||||
<p><img src="images/leader1.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
When we click OK, this is what we see:
|
||||
|
||||
|
||||
<p><img src="images/leader2.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
On the left, we see a failing transition starting in state `0`, using
|
||||
one of our two exported actions, `app.async` and `trans.recv`. To
|
||||
|
|
@ -364,7 +364,7 @@ could start selecting relations to see more information, but let's
|
|||
instead choose the command `Invariant|Diagram` to see what information
|
||||
IVy thinks might be relevant to the failure. Here's what we see:
|
||||
|
||||
|
||||
<p><img src="images/leader3.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
The arrow from id 0 to id 1 is depicting the relation `X:id.t < Y`.
|
||||
Because the arrow goes from `X` to `Y`, we interpret the arrow to mean
|
||||
|
|
@ -379,18 +379,18 @@ to become leader, but it does not have highest id. This situation
|
|||
clearly has to be ruled out. We do this by selecting the
|
||||
`Conjecture|Strengthen` command. Here is what IVy says:
|
||||
|
||||
|
||||
<p><img src="images/leader4.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
In other words, we conjecture that it never happens that a node N has
|
||||
id less than a node P, and node N is receiving its own id. Now we choose
|
||||
`Invariant|Check induction` again, to see if our conjecture is inductive.
|
||||
Of course, it isn't. Here's what Ivy says:
|
||||
|
||||
|
||||
<p><img src="images/leader5.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
And here is the counterexample to induction:
|
||||
|
||||
|
||||
<p><img src="images/leader6.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Here, some externally called action transitions from state `0`
|
||||
satisfying our conjecture to state `1` *not* satisfying the
|
||||
|
|
@ -398,7 +398,7 @@ conjecture. IVy is depicting state `0`, with all the relations that
|
|||
appear in the conjecture. It's not immediately clear what's wrong here,
|
||||
so let's try `Invariant|Diagram` again to see what IVy thinks:
|
||||
|
||||
|
||||
<p><img src="images/leader7.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Now we can see the problem: node 1's id is arriving at node 0, but it
|
||||
should never have passed node 2, because node 2 has a higher
|
||||
|
|
@ -410,14 +410,14 @@ trick up our sleeve. We can use bounded checking to see if some arrows
|
|||
can be removed. We choose `Conjecture|Minimize` and (somewhat
|
||||
arbitrarily) select a bound of 4 steps. Here is what IVy says:
|
||||
|
||||
|
||||
<p><img src="images/leader8.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This conjecture says that we never have nodes in the order `N < P < Q`
|
||||
such that `P` has a smaller id than `Q` and the id of `P` is arriving
|
||||
at `N`. In the graph, we see that the highlights have been removed
|
||||
from the two irrelevant arrows:
|
||||
|
||||
|
||||
<p><img src="images/leader9.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
IVy discovered that, within 4 steps, we
|
||||
can rule out the highlighted facts. By ruling out a more general
|
||||
|
|
@ -429,7 +429,7 @@ Now let's try `Invariant|Check induction` again. IVy is still unhappy
|
|||
and says that our first conjecture is still not relatively inductive. We
|
||||
try `Invariant|Diagram` again and here is what we see:
|
||||
|
||||
|
||||
<p><img src="images/leader10.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This looks very similar to the diagram that led to our previous
|
||||
conjecture. Here, however, it's the id of node 0 that is arriving at
|
||||
|
|
@ -441,7 +441,7 @@ we'll see a way to avoid this symmetry breaking. For now, though,
|
|||
we'll just slog through the cases. As before, we minimize this
|
||||
diagram by bounded checking. Here is the result:
|
||||
|
||||
|
||||
<p><img src="images/leader11.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
IVy conjectures that we do not have nodes `N < P < Q` such that `N`
|
||||
has a lower id than `P` and the id of `N` is arriving at `Q`. This is
|
||||
|
|
@ -453,17 +453,17 @@ Now we try `Invariant|Check induction` (the reader may be able to
|
|||
guess what happens next). Again, IVy says that our first conjecture is
|
||||
not relatively inductive. After `Invariant|Diagram`, we see this:
|
||||
|
||||
|
||||
<p><img src="images/leader12.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This describes the same situation, where the id of node 2 is arriving at node 1.
|
||||
Once again, we generalize using `Conjecture|Minimize`, giving this conjecture:
|
||||
|
||||
|
||||
<p><img src="images/leader13.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
We add this conjecture using `Conjecture|Strengthen`. Now when we
|
||||
use `Invariant|Check induction`, we get the following:
|
||||
|
||||
|
||||
<p><img src="images/leader14.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
That is, we have found a proof for the isolate. We can save this invariant to
|
||||
a file using the `File|Save invariant` command. We edit these conjectures
|
||||
|
|
@ -548,7 +548,7 @@ Now, let's try to verify the isolate `iso_app` with this new version of `ring_to
|
|||
|
||||
As before, after `Invariant|Check induction` and `Invariant|Diagram`, this is what we see:
|
||||
|
||||
|
||||
<p><img src="images/leader15.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
That is, we have a node `1` that is receiving its own id while node
|
||||
`0` has a greater id. Notice, though, that on the right the relation
|
||||
|
|
@ -561,7 +561,7 @@ Now, as before, let's add this as a conjecture using
|
|||
that this conjecture is not relatively inductive. Applying `Invariant|Diagram`,
|
||||
this is what we see:
|
||||
|
||||
|
||||
<p><img src="images/leader16.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This is similar to what we saw before, but notice the blue arrow from
|
||||
node `0` to node `1`. This corresponds to a new relation that has
|
||||
|
|
@ -577,14 +577,14 @@ in this case, there is no effect. No matter -- since this looks like a
|
|||
reasonable conjecture, we use `Conjecture|Strengthen` to add it to our
|
||||
invariant. Here is the result:
|
||||
|
||||
|
||||
<p><img src="images/leader17.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
This says it is not possible to have nodes `Q,N,P` in ascending order of id,
|
||||
such that `N` is on the way from `Q` to `P` and the id of `N` is arriving at `Q`.
|
||||
|
||||
Now let's try `Invariant|Check induction`:
|
||||
|
||||
|
||||
<p><img src="images/leader18.png" alt="Testing IVy screenshot" /></p>
|
||||
|
||||
Because we haven't broken the rotational symmetry of the ring, there
|
||||
is just one case needed when we state the key invariant that an id
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ process observed at different interfaces. That is, TCP is sandwiched
|
|||
between a higher-level application (say, a web browser and web server)
|
||||
and the lower-level datagram protocol (typically the IP protocol) as shown below:
|
||||
|
||||
|
||||
<p><img src="../images/network_stack1.png" alt="Network Stack" /></p>
|
||||
|
||||
The TCP service specification describes the events we observe at the
|
||||
interface between the application layer and the transport layer. The
|
||||
|
|
|
|||
|
|
@ -60,7 +60,7 @@ that only the node with the maximum `id` value can be elected.
|
|||
Our protocol consists of a collection of concurrent process layered on
|
||||
top of two services: a network service and a timer service:
|
||||
|
||||
|
||||
<p><img src="leader_fig1-crop-1.png" alt="Leader Election Ring Figure 1" /></p>
|
||||
|
||||
Let's consider now the two intermediate interfaces. The specification
|
||||
for the network service is quite simple and comes from IVy's standard
|
||||
|
|
@ -179,7 +179,7 @@ would increase the amount of time needed to see an election event.
|
|||
We're going to divide the system into three isolates, one for each of
|
||||
its major components. Here is what the three isolates will look like:
|
||||
|
||||
|
||||
<p><img src="leader_fig2-crop-1.png" alt="Leader Election Ring Figure 2" /></p>
|
||||
|
||||
Here are the isolate definitions:
|
||||
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ process observed at different interfaces. That is, TCP is sandwiched
|
|||
between a higher-level application (say, a web browser and web server)
|
||||
and the lower-level datagram protocol (typically the IP protocol) as shown below:
|
||||
|
||||
|
||||
<p><img src="../../images/network_stack1.png" alt="Network Stack" /></p>
|
||||
|
||||
The TCP service specification describes the events we observe at the
|
||||
interface between the application layer and the transport layer. The
|
||||
|
|
@ -425,7 +425,7 @@ will do something:
|
|||
|
||||
Here is the call graph of the system we have defined:
|
||||
|
||||
|
||||
<p><img src="pingpong_fig1-crop-1.png" alt="Ping Pong Call Graph" /></p>
|
||||
|
||||
Now what we want to do is to generate testers for the left and right
|
||||
players in isolation. That is, we want the tester for the left player
|
||||
|
|
@ -445,7 +445,7 @@ separate verification problems called "isolates".
|
|||
|
||||
Here's the call graph for the left player isolate `iso_l`:
|
||||
|
||||
|
||||
<p><img src="pingpong_fig2-crop-1.png" alt="Ping Pong Call Graph 2" /></p>
|
||||
|
||||
We can see what the first isolate looks like textually as follows (leaving a few
|
||||
things out):
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче