Formal Verification of Systems Software

The first few submissions for project 01 have made me notice that, while the project file is correct, it allows for certain kinds of unfortunate typos that may make your proof meaningless. I cannot guard against the majority of them, obviously, but in an attempt to better evaluate your skills in the project I have added a pseudo_liveness proof obligation (akin to the ones you have seen before in exercises) for exercise01.rs that will hopefully help you catch certain careless mistakes.

You will need to apply the following delta. I have also uploaded a new corrected handout for you to check against, and in case you have not started on the project yet.

I am also distributing a patch that should apply cleanly to your exercise01.rs: you can find it in Materials. To apply it, in a terminal, cd into the directory with handout files and run

patch -p1 < Patch_for_Project_01_Distributed_Lock_Server.patch

(you will need to adjust the path depending on where you downloaded the patch). patch will store the original version of the file with the extension .orig in case you think something went wrong. Regardless, I recommend making a copy of your work so far before applying the patch.

Note that the auto-grader will only accept the new version of the exercise. If you have not started, or have just started, I recommend just re-downloading the handout.

This is the delta to apply (be careful of empty lines).

--- a/exercise01.rs
+++ b/exercise01.rs
@@ -324,6 +324,42 @@ pub mod safety {
         }
     }
 
+    // Show a behavior that the system can transfer the lock from host 0 to host 1
+    // in a distributed system with two hosts.
+    proof fn pseudo_liveness(c: Constants) -> (behavior: Seq<State>)
+        requires
+            c == (Constants {
+                hosts: seq![host::Constants { num_hosts: 2, my_id: 0 }, host::Constants { num_hosts: 2, my_id: 1 }],
+                network: network::Constants { num_hosts: 2 },
+            }),
+        ensures
+            // grouped in one ensures to prevent spurious recommendation failures
+            ({
+                &&& 0 < behavior.len()
+                &&& init(c, behavior[0])
+                &&& host_holds_lock(c, behavior[0], 0)
+                &&& host_holds_lock(c, behavior.last(), 1)
+                &&& behavior.last().well_formed(c)
+                &&& safe(c, behavior.last())
+            }),
+            forall|i:nat| i < behavior.len() - 1 ==> next(c, #[trigger] behavior[i as int], behavior[(i+1) as int]),
+    {
+        /*{*/
+        // let s1 = ...
+        /*}*/
+        let behavior = /*{*/ seq![]/*}*/;
+        assert(0 < behavior.len());
+        assert(init(c, behavior[0]));
+        assert(host_holds_lock(c, behavior[0], 0));
+        assert(host_holds_lock(c, behavior.last(), 1));
+        assert(behavior.last().well_formed(c));
+        assert(safe(c, behavior.last()));
+        assert(forall|i:nat| i < behavior.len() - 1 ==>
+            next(c, #[trigger] behavior[i as int], behavior[(i+1) as int]));
+        behavior
+    }
+
+
 }
 
 } // verus!