Introduction to Murphi3.1 - IV
Published:
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 toy example in Murphi3.1.
In this post, I will go through small extension to toy example using murphi3.1, based on what I have discussed in earlier posts.
SMALL EXTENSION TOY-EXAMPLE - Simple File Management System
This example is adapted from MSI Protocol.
We extend the File Management System which we explain in the previous post, to support either multiple readers can read the file or only one writer can write the file with less bus transactions. We define this model by a simple Finite state machine with following states,
Unused
- No one uses the filesShared
- File is read by one or more peopleModified
- File is modified by one of the person
In this model, we split the Used
states to two states Shared
and Modified
.
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,
};
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;
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.
procedure SendMessage(msg: Message; i: Proc);
begin
switch msg.mtype
case Invalidate:
proc_state[i].state := FS_UNUSED;
proc_state[i].value := undefined;
endswitch;
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_USED)
==>
p.state := FS_USED;
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 data"
(p.state = FS_UNUSED | p.state = FS_USED)
==>
p.state := FS_USED;
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;
undefine last_write;
undefine send_msg;
endstartstate;
At the beginning all the person systems in Unused
state for the particular file and file is in Undefined
.
As a last step we add one additional thing that is Invariant. Invariant describes how valid system should be,
Invariant "only one person in Write 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 "values in valid state match last write"
ForAll n : Proc Do
proc_state[n].state = FS_USED |
proc_state[n].state = FS_MODIFIED
->
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.
- First combine the entire codes and make a murphi file.
- Then generate
.C
file using the murphi file. - Then produce the executable file using
make
command and run.
In the next post, I will talk about how to fully extend this this extended file system.
Hope you enjoyed this post.