Code (Week 1 Thursday) Term 2, 2020 Announcements Course Outline Course Schedule Glossary Maths Resources Moodle - BB Collab Piazza Forum Assignment 0 Spec TeX Guide Web Submission Assignment 1 Spec TeX Guide Web Submission Assignment 2 Spec Web Submission Java Resources Monitors Video Multithreading Video Semaphores Video Volatile Video Web Tutorials Week 1 Homework Monday Board Recording Slides Condensed Slides Thursday Code Slides Condensed Slides Week 2 Homework Thursday Slides Condensed Slides Week 3 Homework Monday Brownies Promela Samples Slides Condensed Slides Thursday Code Slides Condensed Slides Week 4 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 5 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 7 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 8 Homework Monday Slides Thursday Slides Week 9 Homework Monday Slides Thursday Slides Week 10 Notes Code (Week 1 Thursday) Table of Contents 1. Promela Examples 1.1. Hello World 1.2. Counters 2. Critical Section Solutions 2.1. Header File 2.2. Attempt 1 2.3. Attempt 2 2.4. Attempt 3 2.5. Attempt 4 2.6. Attempt 5 (Dekker's Algorithm) 1 Promela Examples 1.1 Hello World proctype A() {
printf("Hello world, I am process %d!\n",_pid);
}
init {
run A();
run A();
}
1.2 Counters #define TIMES 10
byte n = 0;
proctype P() {
byte i =0;
byte temp;
do
:: i < TIMES ->
d_step {
temp = n;
n = temp + 1;
i = i + 1;
}
:: else -> break;
od
}
init {
atomic {
run P();
run P()
}
(_nr_pr == 1);
printf("The value is %d\n", n);
assert(n >= 2);
}
2 Critical Section Solutions 2.1 Header File inline critical_section() {
printf("MSC: %d in CS\n", _pid);
}
inline non_critical_section() {
printf("MSC: %d in non-CS\n", _pid);
do /* non-deterministically choose how
long to stay, even forever */
:: true ->
skip
:: true ->
break
od
}
2.2 Attempt 1
#include "critical2.h"
byte turn = 1;
active proctype p() {
do
:: non_critical_section();
wap: turn == 1; /* await */
csp: critical_section();
turn = 2
od
}
active proctype q() {
do
:: non_critical_section();
waq: turn == 2; /* await */
csq: critical_section();
turn = 1
od
}
2.3 Attempt 2 #include "critical2.h"
bool wantp = false, wantq = false;
active proctype p() {
do
:: non_critical_section();
wap: wantq == false; /* await */
wantp = true;
csp: critical_section();
wantp = false
od
}
active proctype q() {
do
:: non_critical_section();
waq: wantp == false; /* await */
wantq = true;
csq: critical_section();
wantq = false
od
}
2.4 Attempt 3 #include "critical2.h"
bool wantp = false, wantq = false;
active proctype p() {
do
:: non_critical_section();
wap: wantp = true;
wantq == false; /* await */
csp: critical_section();
wantp = false
od
}
active proctype q() {
do
:: non_critical_section();
waq: wantq = true;
wantp == false; /* await */
csq: critical_section();
wantq = false
od
}
2.5 Attempt 4 #include "critical2.h"
bool wantp = false, wantq = false;
active proctype p() {
do
:: non_critical_section();
wap:
wantp = true;
do
:: wantq -> wantp = false; wantp = true ;
:: else -> break ;
od;
csp: critical_section();
wantp = false
od
}
active proctype q() {
do
:: non_critical_section();
waq: wantq = true;
do
:: wantp -> wantq = false; wantq = true ;
:: else -> break ;
od;
csq: critical_section();
wantq = false
od
}
ltl mutex { always (!(p@csp && q@csq)) }
ltl sf { always (p@wap implies eventually p@csp)}
2.6 Attempt 5 (Dekker's Algorithm) #include "critical2.h"
bool wantp = false, wantq = false;
byte turn = 1;
active proctype p() {
do
:: non_critical_section();
wap:
wantp = true;
do
:: wantq ->
if
:: turn == 2 ->
wantp = false;
/* await */ turn == 1;
wantp = true;
:: else -> skip;
fi
:: else -> break;
od
csp: critical_section();
turn = 2;
wantp = false
od
}
active proctype q() {
do
:: non_critical_section();
waq: wantq = true;
do
:: wantp ->
if
:: turn == 1 ->
wantq = false;
/* await */ turn == 2;
wantq = true;
:: else -> skip;
fi
:: else -> break;
od
csq: critical_section();
turn = 1;
wantq = false
od
}
ltl mutex { always (!(p@csp && q@csq)) }
ltl sf { always (p@wap implies eventually p@csp)}
2020-08-06 Thu 03:32 Announcements RSS
