Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
An Invalid (Deadlocked) Model of Resource Sharing Problem
/*
* Resource Sharing Problem (Example for Deadlock)
*/
mtype = { LOCK, UNLOCK };
proctype Client(chan to_res1, to_res2) {
if
:: to_res1 ! LOCK(_pid);
to_res2 ! LOCK(_pid);
:: to_res2 ! LOCK(_pid);
to_res1 ! LOCK(_pid);
fi;
if
:: to_res1 ! UNLOCK(_pid);
to_res2 ! UNLOCK(_pid);
:: to_res2 ! UNLOCK(_pid);
to_res1 ! UNLOCK(_pid);
fi
}
proctype Resource(chan to_res) {
pid locker;
pid unlocker;
end:
do
:: to_res ? LOCK(locker);
to_res ? UNLOCK(unlocker);
assert(locker == unlocker);
od
}
init {
chan to_scanner = [0] of { mtype, pid };
chan to_printer = [0] of { mtype, pid };
atomic {
run Client(to_scanner, to_printer);
run Client(to_scanner, to_printer);
run Resource(to_scanner);
run Resource(to_printer);
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.