EECS 570: Murphi Tutorial

An introductory tutorial on protocol verification using Murphi.





Step 0: Protocol State Diagram

We will verify a simple client server protocol -- lock server.
The smallest non-trivial instance has one server and two clients.
A client can perform two actions: connect and disconnect.
The server uses a lock to ensure that only one client is connected at a time.

Verification requires specifying the complete system as a state transition system.





Step 1(a): Protocol Specification

Murphi description language:
 Vars represent states; are of Type (can be user-defined).
 Rule describes a transition; has pre-condition and action.

Let's specify our system using Murphi. 

Var server_lock : boolean;
Var client0_link, client1_link : boolean;

StartState
Begin
	server_lock := true;
	client0_link := false;
	client1_link := false;
End;

Rule "client 0 connect"
	server_lock
==>
Begin
	client0_link := true;
	server_lock := false;
End;
      
Rule "client 1 connect"
	server_lock
==>
Begin
	client1_link := true;
	server_lock := false;
End;

Rule "client 0 disconnect"
	client0_link
==>
Begin
	client0_link := false;
End;
      
Rule "client 1 disconnect"
	client1_link
==>
Begin
	client1_link := false;
End;

Compile and run:

  1. Compile Murphi code: generates C code. 
    $ ./mu lockserver.m
Code generated in file lockserver.C
  2. Compile generated C code: generates executable binary. 
    $ make lockserver
g++ -DCATCH_DIV  -Wno-write-strings -m32  -o lockserver lockserver.C -I../include -lm
  3. Run 
    $ ./lockserver
Result:
        Deadlocked state found.

Protocol Deadlock: Specification is incorrect.
Murphi reports violation trace 

$ ./lockserver -tv
The following is the error trace for the error:

        Deadlocked state found.

Startstate Startstate 0 fired.
server_lock:true
client0_link:false
client1_link:false
----------

Rule client 1 connect fired.
server_lock:false
client1_link:true
----------

Rule client 1 disconnect fired.
The last state of the trace (in full) is:
server_lock:false
client0_link:false
client1_link:false
----------

End of the error trace.
!! We forgot to release lock back to server.

Rule "client 0 disconnect"
	client0_link
==>
Begin
	client0_link := false;
	server_lock := true;
End;
      
Rule "client 1 disconnect"
	client1_link
==>
Begin
	client1_link := false;
	server_lock := true;
End;

Compile and run (output): 

$ ./lockserver
Status:
        No error found.

State Space Explored:
        3 states, 4 rules fired in 0.10s.

Step 1(b): Protocol Correctness -- "only one client is connected at a time".
 Invariant specifies a property that always holds.

Invariant "only one client at a time"
	!server_lock & ((client0_link & !client1_link) | (!client0_link & client1_link))

Compile and run (output): 

$ ./lockserver
Result:
        Invariant "only one client at a time" failed.

$ ./lockserver -tv
The following is the error trace for the error:

        Invariant "only one client at a time" failed.

Startstate Startstate 0 fired.
server_lock:true
client0_link:false
client1_link:false
----------

End of the error trace.
!! Our invariant fails on start state itself. Let's fix the invariant. 
Invariant "only one client at a time"
	server_lock | !server_lock & ((client0_link & !client1_link) | (!client0_link & client1_link))

OR write better invariant. 

Invariant "only one client at a time"
	 !(client0_link & client1_link)

Compile and run (output): 

$ ./lockserver
Status:
        No error found.

State Space Explored:
        3 states, 4 rules fired in 0.10s.

[source]



Step 2: Modularity
Note that rules for (dis)connect are similar for each client. No need to duplicate logic!
Also, modular design would easily allow increasing number of clients.

 RuleSet applies rules using induction variables.
 ForAll iterates over the range of induction variables.

[source] 

Type
	server_t : Record
		lock : boolean;
	End;
	client_t : Record
		link : boolean;
	End;
	client_n: 0..1;

Var
	server : server_t;
	client : Array[client_n] of client_t;

StartState
Begin
	server.lock := true;
	For c : client_n Do
		client[c].link := false;
	End;
End;

RuleSet c : client_n Do
	Rule "client connect"
		server.lock
	==>
	Begin
		client[c].link := true;
		server.lock := false;
	End;
      
	Rule "client disconnect"
		client[c].link
	==>
	Begin
		client[c].link := false;
		server.lock := true;
	End;
End;

Invariant "only one client at a time"
	ForAll c : client_n Do
		!(client[c].link & client[1-c].link)
	End;

Compile and run (output): 

$ ./lockserver -pr
Status:
        No error found.

State Space Explored:
        3 states, 4 rules fired in 0.10s.

Rules Information:
        Fired 1 times   - Rule "client disconnect, c:0"
        Fired 1 times   - Rule "client disconnect, c:1"
        Fired 1 times   - Rule "client connect, c:0"
        Fired 1 times   - Rule "client connect, c:1"
Let's increase the number of clients. What changes are needed? 
Invariant "only one client at a time"
	ForAll c1 : client_n Do
	ForAll c2 : client_n Do
        	client[c1].link & client[c2].link
		->
		c1 = c2
	End
End;

10 clients

Compile and run (output): 

$ ./lockserver
Status:
        No error found.

State Space Explored:
        11 states, 20 rules fired in 0.10s.

100 clients

Compile and run (output): 

$ ./lockserver
State Space Explored:
        101 states, 200 rules fired in 0.10s.

1000 clients

Compile and run (output): 

$ ./lockserver
Error:
        Internal Error: Too many active states.
!! Verifying all states explicitly is unscalable for large systems.



Step 3: Symmetry for scalability

 ScalarSet is an unordered enumeration type that allows Murphi to leverage symmetry.
 MultiSet is an unordered map with symmetry.

[source] 

Const
	numClient: 10;

Type
	server_t : Record
		lock : boolean;
	End;
	client_t : Record
		link : boolean;
	End;
	client_n: ScalarSet(numClient);

Var
	server : server_t;
	client : Array[client_n] of client_t;

StartState
Begin
	server.lock := true;
	For c : client_n Do
		client[c].link := false;
	End;
End;

RuleSet c : client_n Do
	Rule "client connect"
		server.lock
	==>
	Begin
		client[c].link := true;
		server.lock := false;
	End;
      
	Rule "client disconnect"
		client[c].link
	==>
	Begin
		client[c].link := false;
		server.lock := true;
	End;
End;

Invariant "only one client at a time"
	ForAll c1 : client_n Do
	ForAll c2 : client_n Do
		client[c1].link & client[c2].link
		->
			c1 = c2
	End
	End;

10 clients

Compile and run (output): 

$ ./lockserver
State Space Explored:
        2 states, 11 rules fired in 0.10s.

100 clients

Compile and run (output): 

$ ./lockserver
State Space Explored:
        2 states, 101 rules fired in 0.10s.

$ ./lockserver -nosym
State Space Explored:
        101 states, 200 rules fired in 0.10s.

1000 clients

Compile and run (output): 

$ ./lockserver
State Space Explored:
        2 states, 1001 rules fired in 12.17s.
!! With 100 clients, instead of verifying 101 explicit states, it is sufficient to verify only 2 symmetric states.
Using symmetry is key for scalable verification of complex systems.



Useful Murphi options: