Example Models for APNN-ToolBox
This Net is divided into two sections(Left-section (refered as l) and Right-section (refered as r)).Reader is on right side and Writer is on left side.
Different sites may be given different prioritieshence different access policies to their respective critical regions.
A typical example is a system of a writer and a reader site of a shared variable: whenever prepared to update the
variable, the writer may eventually execute this update in its critical state. The reader may be guaranteed less:
whenever pending for reading the variable, the reader will eventually get reading or the writer will eventually
update the variable. Hence the reader may start to access its critical state in vain. 13.9 shows this algorithm.
It uses three flags. The flag 'writer_detached' signals to the reader that the writer is presently not striving
to become 'writing'. The flag 'reader_detached' likewise signals to the writer that the reader is presently not
striving to become 'reading'. The flag 'writer_involved' is just the complement of 'writer_detached': Exactly one
of them is visible at any time. After finishing the production of a new value along the quiescent action a, the writer
takes two steps to reach its critical state, 'writing'. In the first step, the fair action b just swaps the flag
'writer_detached' to 'writer_involved'. Fairness of action b is apparently local. The second step brings the writer
to its critical state, 'writing', along the action c. The overall structure of the algorithm guarantees that the flag
'reader_detached' eventually remains until c has occurred. After using the previous value of the shared variable,
the reader may become pending for a new value along the quiescent action e. It takes the reader two steps to reach
its critical state, 'reading'. Neither of them is guaranteed to occur. Furthermore, the reader in the intermediate
state pend2 may be forced to return to pend1. By the first action, f, the reader removes the 'reader_detached' flag.
Iterated occurrence of action c may prevent the occurrence of f. The second step from pend2 to reading with action g,
is possible only in case the writer is detached. In case the writer is involved instead, action j releases the flag
'reader_detached', allowing the writer to proceed. The reader remains in state failed until the writer is detached.
In this case, the reader may proceed to pend1 and starts further attempt to get reading.
Download APNN Description of the model.