Introduction to Murphi3.1 - V

The model I describe in the toy example is not fully specified. So in the real -world, it can reach a failure states. Thise purpose of these series of posts aims to get into hands with how to implement verification from specified system Murphi3.1.

This is the continuation of previous post which provides a small extension to toy example in Murphi3.1.

In this post, I will go through full extension toy example using murphi3.1, based on what I have discussed in earlier posts.

FULLY EXTENDED TOY-EXAMPLE - Simple File Management System

This example is adapted from MESI Protocol.

We further extend the File Management System which we explain in the previous post, to support either exclusive access to read and write when only one person read or write, and avoid unwanted bus transactions. We define this model by a simple Finite state machine with following states,

1. Unused - No one uses the files
2. Shared - File is read by more than persons
3. Exclusive - File is read by only one person
4. Modified - File is modified by one of the person

In this model, we split the Shared states to two states Shared and Exclusive.

Next we define, how the communication are happen, The file (or data) in main-memory and it will loaded into virtual/private memory of individual users when they call a Read or Write command. The communication happen through a bus which connects all the users and main-memory and when ever some user send either Read or Write command, it will communicate to the main memory and obtain the copy and use it.

Detailed State Diagram.

Now we look into how we simply convert this state diagram into murphi verification code.

Consider there is only one file and 3 people have access to the file. Those three people can either Read or Write the file.

First we define the constants, types and variables required to define the simple file system,

const
	person_count: 3;
	file_count: 1;

type
  	Proc : scalarset(person_count);
	Value: scalarset(file_count);
	ProcState:
	record
		state: enum { 
			FS_UNUSED,
			FS_SHARED,
			FS_MODIFIED,
			FS_EXCLUSIVE,
		};
		value: Value;
	end;

	MessageType: enum {  
	    Invalidate,
	}; 

	Message:
    record
      mtype: MessageType;
	  value: Value;
    end;
 
var
	proc_state: array[Proc] of ProcState;
	last_write: Value;
    send_msg: Message;
    transaction_flag: boolean;

In above description, we add additional variable transaction_flag which used to define whether one process is already reading the file or not. Depending on the transaction_flag, when a person call Read command the person will go to Exclusive (if transaction_flag := false) or Shared ( if transaction_flag := true).

Next we define the method SendMessage to send messages through bus to other person, when ever someone starts writing. This function will invalidate and move to the state Unused, when ever some one write. Also this function will make the exclusive access to shared access when more than one person actually starts read the file.

procedure SendMessage(msg: Message; i: Proc);
begin
	switch msg.mtype
		case ReadShared:
			if (proc_state[i].state = FS_MODIFIED | 
				proc_state[i].state = FS_EXCLUSIVE) then
				proc_state[i].state :=  FS_SHARED;
			endif;

		case ReadModified:
			proc_state[i].state :=  FS_UNUSED;

		case Invalidate:
			proc_state[i].state :=  FS_UNUSED;

	endswitch;
    proc_state[i].value := msg.value;
	if (proc_state[i].state = FS_UNUSED) then
		proc_state[i].value := undefined;
	endif;
end;

Thereafter we have two define the rulesets for Read and Write commands as shown below.

ruleset i: Proc do
  	alias p: proc_state[i] do
  		ruleset v: Value do
			rule "Write data"
				(p.state = FS_UNUSED | p.state = FS_SHARED | p.state = FS_MODIFIED)
			==>
				p.state :=  FS_MODIFIED;
				p.value := v;
				last_write := v;

		        for k:Proc do
					if i != k then
						send_msg.mtype := Invalidate;
						send_msg.value := undefined;
						SendMessage(send_msg, k);
					endif;
				endfor;
			endrule;
        endruleset;

    rule "Read Exclusive data"
            (p.state = FS_UNUSED | p.state = FS_SHARED | ~transaction_flag)
        ==>
            p.state :=  FS_EXCLUSIVE;
            p.value := last_write;
            transaction_flag := true;
        endrule;
  	endalias;
    
    rule "Read Shared data"
            (p.state = FS_UNUSED | p.state = FS_SHARED | transaction_flag)
        ==>
            p.state :=  FS_SHARED;
            p.value := last_write;
        endrule;
  	endalias;
endruleset;

After that, we define the start states as follows,

startstate
	for i: Proc do
		proc_state[i].state := FS_UNUSED;
	endfor;
  transaction_flag := false;
  undefine last_write;
  undefine send_msg;
endstartstate;

At the beginning all the person systems in Unused state for the particular file, file is in Undefined and at the start since no one is actually using the file the transaction_flag is set to false.

As a last step we add one additional thing that is Invariant. Invariant describes how valid system should be,

Invariant "only one person in Modified state"
ForAll p1 : Proc Do
	ForAll p2 : Proc Do
		proc_state[p1].state = FS_MODIFIED & proc_state[p2].state = FS_MODIFIED
		->
			p1 = p2
	End
	End;

Invariant "only one person in Exclusive state"
ForAll p1 : Proc Do
	ForAll p2 : Proc Do
		proc_state[p1].state = FS_EXCLUSIVE & proc_state[p2].state = FS_EXCLUSIVE
		->
			p1 = p2
	End
	End;

Invariant "values in valid state match last write"
  ForAll n : Proc Do  
    proc_state[n].state = FS_SHARED | proc_state[n].state = FS_MODIFIED | proc_state[n].state = FS_EXCLUSIVE
    ->
    proc_state[n].value = last_write 
  End;

Invariant "value is undefined while invalid"
  ForAll n : Proc Do  
    proc_state[n].state = FS_UNUSED
    ->
    IsUndefined(proc_state[n].value)
  End;

Finally, we need to work on how to actually compile this and verify the system.

1. First combine the entire codes and make a murphi file.
2. Then generate .C file using the murphi file.
3. Then produce the executable file using make command and run.

For more complex models look at my previous post which is based on Futurebus+ protocol.

1. Futurebus+ Protocol
2. Fix on Futurebus+ Protocol

Hope you enjoyed this post.