ESERCIZI CFSM e proprieta' di sistemi concorrenti.
Esercizio 0
Describe the two CFSMs system representing the following simple protocol between two processes, USER and SERVER.
Initially, both are in their initial states (READY and IDLE).
USER can send a request (message REQ) to SERVER.
After receiving REQ, SERVER enters state SERVICE; when it is finished with the service, it goes back to state IDLE while sending the message DONE to USER.
Between sending REQ and receiving DONE, USER stays in state WAIT.
While idle, SERVER can detect a fault in itself.
If so, it informs USER about it by sending the message ALARM.
When USER receives an ALARM, it registers it and directs SERVER back to its IDLE state by the message ACK.
[Example by Brand and Zafiropulo]
Esercizio 1
Describe as CFSMs system the protocol
ATM that specifes an ATM
scenario. The protocol
involves three roles: a client (C), the
payment server (S) and a separate authenticator (A).
At the start of the protocol, C sends its login details
to A, then A informs S and C
whether the authentication is successful,
by choosing either a success or a failuse.
In the former case C and S
enter a transaction loop. In each iteration, S
sends C the amount available in
the account. Next, C has three choices:
- withdraws an amount and repeats the loop;
- deposits an amount in the account and repeats the loop;
- ends the transaction.
Esercizio 2
Describe as CFSMs system the following protocol.
Consider two buyers, Buyer1 and Buyer2.
They wish to buy an expensive book from Seller by combining their
money. Buyer1 sends the title of the book to Seller, Seller sends
to both Buyer1 and Buyer2 its quote, Buyer1 tells Buyer2 how
much she can pay, and Buyer2 either accepts the quote or receives
the quote by notifying Seller.
Esercizio 3
Consider two user processes that share a common resource and synchronize their activities by exchanging messages via two one-directional, unbounded, FIFO channels. Occasionally, each user enters its critical section to access the common resource. The following protocol is a synchronization mechanism proposed by Chandy and Misra such that at any instant, at most one user is in its critical section.
Describe the protocol as a CFSMs system.
I. Initially, exactly one user has the right to its critical section.
II. If a user has the right to its critical section, then it can enter its critical section any number of times provided that it frequently examines its input channel from the other user to check whether it has a request message. If it finds a request message, it sends an acknowledgement message to the other user, thus giving up the right to the critical section to the other user. If it finds no re- quest, it keeps the right to its critical sec- tion.
III. If a user has no right to its critical section, it can send a request message to the other user asking for it. Then, when it receives an acknowledgement, it has the right to its critical section.
Possibile soluzione.
Esercizio 4
Un sistema di CFSMs soddisfa la proprieta' P se per ogni s∈RS(S) esiste s' finale tale che
s→*s'.
La proprieta' P e' una safety property o una liveness property. Giustificare la risposta.
Esercizio 5
Un sistema di CFSMs soddisfa la proprieta' di strongly boundedness se i contenuti dei buffer di tutte le possibili
configurazioni raggiungibili formano un insieme finito.
s→*s'.
La proprieta' P e' una safety property o una liveness property? Giustificare la risposta.
Esercizio 6 (by S. A. Seshia)
Per ognuna delle seguenti proprieta' dire se e' una safety o una liveness property, fornendone giustificazione.
- No more than one processor (in a multi-processor
system) should have a cache line in write mode
- The grant signal must be asserted at some time
after the request signal is asserted
- Every request signal must receive an
acknowledge and the request should stay asserted
until the acknowledge signal is received
Esercizio 7
Esprimere le proprieta' dell'esercizio 6 in LTL e CTL, utilizzando i seguenti simboli proposizionali:
- wr1
/ wr2 are respectively true if processor 1 / 2 has the
line in write mode;
- Signals: grant, req;
- Signals: req, ack
Esercizio 8
Esercizio 9
Esercizio 10
Esercizio XX
Possibile soluzione.