Mutual Exclusion in Two-Process Semaphore System with Fairness Analysis

request = TRUE

state = busy

Trace Description: Simulation Trace

Trace Type: Simulation

-> State: 2.1 <-

request = TRUE

state = ready

-> State: 2.2 <-

state = busy

-> State: 2.3 <-

request = FALSE

-> State: 2.4 <-

request = TRUE

-> State: 2.5 <-

request = FALSE

-> State: 2.6 <-

state = ready

-> State: 2.7 <-

NuSMV>

next(semaphore) :=

case

state = entering : TRUE;

state = exiting : FALSE;

TRUE : semaphore;

esac;

FAIRNESS

running

MODULE main

VAR

semaphore : boolean;

proc1 : process user(semaphore);

proc2 : process user(semaphore);

ASSIGN

init(semaphore) := FALSE;

SPEC AG ! (proc1.state = critical & proc2.state = critical)

SPEC AG (proc1.state = entering -> AF proc1.state = critical)

MODULE user(semaphore)

VAR

state : {idle, entering, critical, exiting};

ASSIGN

init(state) := idle;

next(state) :=

case

state = idle : {idle, entering};

state = entering & !semaphore : critical;

state = critical : {critical, exiting};

state = exiting : idle;

TRUE : state;

Esac;

-> State: 1.4 <-

semaphore = FALSE

proc2.state = critical

-> Input: 1.5 <-

_process_selector_ = proc1

-> State: 1.5 <-

-> Input: 1.6 <-

_process_selector_ = proc2

-> State 1.6 <-

proc2.state = exiting

-> Input: 1.7 <-

_process_selector_ = proc2

-> State 1.7 <-

semaphore = FALSE

proc2.state = idle

specification AG (!(proc1.state = critical & proc2.state

= critical))

-- is true

-- specification AG (proc1.state = entering -> AF

proc1.state = critical)

-- is false

-- as demonstrated by the following execution

sequence

-> State: 1.1 <-

semaphore = FALSE

proc1.state = idle

proc2.state = idle

-> Input: 1.2 <-

_process_selector_ = proc1

-- Loop starts here

-> State: 1.2 <-

proc1.state = entering

-> Input: 1.3 <-

_process_selector_ = proc2

-> State: 1.3 <-

proc2.state = entering

-> Input: 1.4 <-

_process_selector_ = proc2