And trail file was generated which shows the errors. Help me
correct my code in writer-and-readers.pml
writerand reader file
// Below here is (c) 2022 Andrew Butterfield, Trinity College
Dublin.
#if defined(ZERO)
#include "pthreads0.pml"
#elif defined(ONE)
#include "pthreads1.pml"
#elif defined(TWO)
#include "pthreads2.pml"
#else /* no number specified */
#include "pthreads.pml"
#endif
// Code below here is a correct model of producer-consumer
behaviour.
// DO NOT MODIFY
// ====== Buffer Model
========================================================
#define BUFSIZE 4
byte buffer[BUFSIZE];
byte in,out;
bool bfull,bempty;
inline zerobuffer() {
in = 0;
do
:: in < BUFSIZE -> buffer[in] = 0; in++
:: else -> in = 0; break
od
out = BUFSIZE-1;
bfull = false; bempty = true;
printf("buffer zeroed\n")
}
byte six;
inline showbuffer(){
atomic{
printf("@@@ %d BUFFER in:%d, out:%d, empty:%d,
full:%d [|",_pid,in,out,bempty,bfull);
six = 0;
do
:: six < BUFSIZE -> printf(" %d
|",buffer[six]); six++;
:: else -> printf("]\n"); break;
od
}
}
#define NEXT(i) ((i+1) % BUFSIZE)
inline insert(x) {
assert(!bfull);
buffer[in] = x;
printf("@@@ %d INSERT buf[%d] := %d\n",_pid,in,x);
bempty = false;
bfull = (in == out);
in = NEXT(in);
showbuffer();
}
byte cout[2];
inline extract(cno) {
assert(!bempty);
out = NEXT(out);
cout[cno] = buffer[out]; buffer[out] = 0;
printf("@@@ %d EXTRACT cout[%d] := buf[%d] is
%d\n",_pid,cno,out,cout[cno]);
bfull = false;
bempty = (NEXT(out) == in)
showbuffer();
}
// ====== Producer Model
======================================================
inline produce(p) {
lock(mtx);
assert(mtx.mid == _pid);
do
:: !bfull -> break;
:: else -> wait(PRODCONDVAR,mtx);
od
insert(p);
progress_prod:
signal(CONSCONDVAR);
unlock(mtx);
}
pthreads file
// pthreads.pml
// Task: modify lock, unlock, wait and signal to do the correct
thing.
mtype = { unlocked, locked } ;
typedef mutexData {
mtype mstate;
byte mid;
// may need more fields here
}
typedef condvarData {
bool dummy;
// may need different fields here
}
mutexData mtx;
condvarData cvars[2];
#define PRODCONDVAR 0
#define CONSCONDVAR 1
inline initsync() {
mtx.mstate = unlocked;
cvars[0].dummy = true;
cvars[1].dummy = true;
// may need more/different code to initialise fields
here
}
// pthread_mutex_lock(&m);
inline lock(m) {
printf("@@@ %d LOCKING : state is
%e\n",_pid,m.mstate)
// will need code here
printf("@@@ %d LOCKED : state is %e\n",_pid,m.mstate)
}
// pthread_mutex_unlock(&m);
inline unlock(m) {
printf("@@@ %d UNLOCKING : state is
%e\n",_pid,m.mstate)
// will need code here
printf("@@@ %d UNLOCKED : state is
%e\n",_pid,m.mstate)
}
// pthread_cond_wait(&c,&m);
inline wait(c,m) {
printf("@@@ %d WAIT for cond[%d]=%d with
mutex=%e\n",_pid,
c,cvars[c].dummy,m.mstate)
// will need code here
printf("@@@ %d DONE with cond[%d]=%d with
mutex=%e\n",_pid,
c,cvars[c].dummy,m.mstate)
}
// pthread_cond_signal(&c);
inline signal(c) {
printf("@@@ %d SIGNAL
cond[%d]=%d\n",_pid,c,cvars[c].dummy)
// will need code here
printf("@@@ %d SIGNALLED
cond[%d]=%d\n",_pid,c,cvars[c].dummy)
}
trail file
- I Was Given Two Files Pthread Pml And Writer And Readers Pml And Trail File Was Generated Which Shows The Errors Help 1 (124.06 KiB) Viewed 27 times
- I Was Given Two Files Pthread Pml And Writer And Readers Pml And Trail File Was Generated Which Shows The Errors Help 2 (70.34 KiB) Viewed 27 times
proctype producer() {
int p=1;
do
:: produce(p); p = p % REPEAT + 1
// should generate 1,...,7,1,...,7,1,...,7,....
od
}
// ====== Consumer Model
======================================================
inline consume(cno) {
lock(mtx);
assert(mtx.mid == _pid);
do
:: !bempty -> break;
:: else -> wait(CONSCONDVAR,mtx);
od
extract(cno);
progress_cons:
signal(PRODCONDVAR);
unlock(mtx);
}
proctype consumer(byte cno) {
do
:: consume(cno)
od
}
// ====== MAINLINE
============================================================
init {
int z;
printf("A Model of pthreads\n")
printf("\n Producer-Consumer example\n")
zerobuffer()
showbuffer()
initsync()
run producer()
run consumer(0)
run consumer(1)
}
asranis@sallu:/mnt/c/usersasranis@sallu:/mnt/c/users/salon/desktop/tcd/hillary term/os$ s pin -p -t writer-and-readers.pml A Model of pthreads proc 0 (:init::1) writer-and-readers.pml:123 (state 1) [printf('A Model of pthreads\\n')] 1: 3: 6: 7: 9: Producer-Consumer example 1: proc 0 (:init::1) writer-and-readers.pml:124 (state 2) [printf('\\n Producer-Consumer example\\n')] 2: proc 0 (:init::1) writer-and-readers.pml:24 (state 3) [in = 0] proc 0 (:init::1) writer-and-readers.pml:26 (state 4) [((in<4))] 4: proc 0 (:init::1) writer-and-readers.pml:26 (state 5) [buffer[in] = 0] 5: proc 0 (:init::1) writer-and-readers.pml:26 (state 6) [in = (in+1)] proc 0 (:init::1) writer-and-readers.pml:26 (state 4) [((in<4)] proc 0 (:init::1) writer-and-readers.pml:26 (state 5) [buffer[in] = 0] 8: proc 0 (:init::1) writer-and-readers.pml:26 (state 6) [in = (in+1)] proc 0 (:init::1) writer-and-readers.pml:26 (state 4) [((in<4))] 10: proc 0 (:init::1) writer-and-readers.pml:26 (state 5) [buffer[in] = 0] 11: proc 0 (:init::1) writer-and-readers.pml:26 (state 6) [in = (in+1)] 12: proc 0 (:init::1) writer-and-readers.pml:26 (state 4) [((in<4))] 13: proc o (:init::1) writer-and-readers.pml:26 (state 5) [buffer[in] = 0] 14: proc 0 (:init::1) writer-and-readers.pml:26 (state 6) [in (in+1)] 15: proc 0 (:init::1) writer-and-readers.pml:27 (state 7) [else] 16: proc 0 (:init::1) writer-and-readers.pml:27 (state 8) [in = 0] 17: proc 0 (:init::1) writer-and-readers.pml:29 (state 13) [out = (4-1)] 18: proc 0 (:init::1) writer-and-readers.pml:30 (state 14) [bfull = 0] 19: proc 0 (:init::1) writer-and-readers.pml:30 (state 15) [bempty = 1] buffer zeroed 20: proc 0 (:init::1) writer-and-readers.pml:31 (state 16) [printf('buffer zeroed\\n')] @@@ O BUFFER in:0, out:3, empty:1, full:0 (| 21: proc 0 (:init::1) writer-and-readers.pml:38 (state 18) [printf('@@@ %d BUFFER in:%d, out:%d, empty:%d, full:%d [| 21: proc 0 (:init::1) writer-and-readers.pm1:39 (state 19) [six = 0] 22: proc 0 (:init::1) writer-and-readers.pml:41 (state 20) [((six<4))] 0 | 22: proc 0 (:init::1) writer-and-readers.pml:41 (state 21) [printf(" %d ', buffer[six])] 22: proc 0 (:init::1) writer-and-readers.pml:41 (state 22) [six = (six+1)] 23: proc 0 (:init::1) writer-and-readers.pml:41 (state 20) [((six<4))] 0 | 23: proco (:init::1) writer-and-readers.pml:41 (state 21) [printf('%d l', buffer[six])] 23: proc 0 (:init::1) writer-and-readers.pml:41 (state 22) [six = (six+1)] 24: proc 0 (:init::1) writer-and-readers.pml:41 (state 20) [((six<4))] 0 | 24: proc 0 (:init::1) writer-and-readers.pml:41 (state 21) [printf('%d ', buffer[six])] 24: proc 0 (:init::1) writer-and-readers.pml:41 (state 22) [six = (six+1)] 25: proc 0 (:init::1) writer-and-readers.pml:41 (state 20) [((six<4))] 0 | 25: proc 0 (:init::1) writer-and-readers.pml:41 (state 21) [printf('%d L', buffer[six])] 25: proc 0 (:init::1) writer-and-readers.pml:41 (state 22) [six = (six+1)] 26: proc 0 (:init::1) writer-and-readers.pml:42 (state 23) [else] 27: proc 0 (:init::1) writer-and-readers.pml:42 (state 24) [printf(']\\n')]
29: 27: proc 0 (:init::1) writer-and-readers.pml:42 (state 24) [printf(']\\n')] 28: proc 0 (:init::1) writer-and-readers.pml:40 (state 28) [break] proc 0 (:init::1) pthreads.pml:26 (state 31) [mtx.mstate = unlocked] 30: proc (:init::1) pthreads.pml:27 (state 32) [cvars[0].dummy = 1] 31: proc 0 (:init::1) pthreads.pml:28 (state 33) [cvars[1]. dummy = 1] Starting producer with pid 1 32: proc 0 (:init::1) writer-and-readers.pml:128 (state 35) [(run producer())] asranis@sallu:/mnt/c/users/salon/desktop/tcd/hillary term/osm/os$ [(run consumer (0))] Starting consumer with pid 3 34: proc 0 (:init::1) writer-and-readers.pml:130 (state 37) [(run consumer(1))] @@@ 3 LOCKING : state is unlocked 35: proc 3 (consumer:1) pthreads.pml:34 (state 1) [printf('@@@ %d LOCKING : state is %e\\n',_pid, mtx.mstate)] @@@ 3 LOCKED : state is unlocked 36: proc 3 (consumer:1) pthreads.pml:36 (state 2) [printf("@@@ %d LOCKED : state is %e\\n',_pid, mtx.mstate)] spin: writer-and-readers.pml:101, Error: assertion violated spin: text of failed assertion: assert((mtx.mid==_pid)) 37: proc 3 (consumer:1) writer-and-readers.pml:101 (state 4) [assert((mtx.mid==_pid))] spin: trail ends after 37 steps #processes: 4 mtx.mstate = unlocked mtx.mid = 0 cvars[0].dummy = 1 cvars[1].dummy = 1 buffer[@] = 0 buffer[1] = 0 buffer[2] = 0 buffer[3] = 0 in = 0 out = 3 bfull = 0 bempty = 1 six = 4 cout[0] = 0 cout[1] = 0 37: proc 3 (consumer:1) writer-and-readers.pml:102 (state 11) 37: proc 2 (consumer:1) writer-and-readers.pml:113 (state 42) 37: proc 1 (producer:1) writer-and-readers.pml:91 (state 42) 37: proc 0 (:init::1) writer-and-readers.pml:131 (state 38) <valid end state> asranis@sallu:/mnt/c/users/salon/desktop/tcd/hillary term/os$