Hi, I understand that Java associates a lock with every shared object to ensure mutual exclusion and condition sync. I am told to model a Java recursive lock as a FSP process.. but I'm stuck and below is the question and what I've written so far. HELP IS GREATLY GREATLY APPRECIATED.
QNS: Given the following declarations:
const N = 3
range P = 1..2 //thread identities
range C = 0..N //counter range for lock
Model a Java recursive lock as the FSP process RECURSIVE_LOCK with the alphabet{acquire[p:P],release[p:P]}. The action acquire[p] acquires the lock for thread p. Once a thread has acquired the lock, it does not have to wait to acquire the lock again. You may assume that the acquire and release actions are atomic.
WHAT I'VE HAD WRITTEN:
const N = 3
range P = 1..2
range C = 0..N
RECURSIVE_LOCK = (acquire[x:P] -> THREAD[x]),
THREAD[i:P] = (read->THREAD[i] | release->RECURSIVE_LOCK).
Please advise me on where I'd gone wrong and I need explanation regarding "recursive lock" and "atomic actions".