Producer Consumer

Lezione del 2018-12-21.

Specifichiamo un sistema di tipo Produttore-Consumatore. In generale il produttore crea un qualche tipo di informazione, che il consumatore riceve.

Ipotizziamo che questo sistema sia in grado di tenere parcheggiate due informazioni.

Le azioni permesse sono il deposito (\(deposit\)) dell’informazione e il suo prelievo (\(withdraw\)).

PC: sequencial specification

Avremo gli stati:

  • nessuna informazione depositata (\(ProdCons02\)),
  • una informazione depositata (\(ProdCons12\)),
  • due informazioni depositate (\(ProdCons22\)).

La gestione degli stati è la seguente.

Senza informazioni depositate, si può solo depositare:

\[ProdCons02 = deposit \cdot ProdCons12\]

Con una informazione depositata è possibile depositarne un’altra oppure prelevare l’informazione presente:

\[ProdCons12 = deposit \cdot ProdCons22 + withdraw \cdot ProdCons02\]

Con due informazioni depositate si può solo prelevare un dato:

\[ProdCons22 = withdraw \cdot ProdCons12\]

Volendo esprimerla come un automa a stati finiti, avremmo la seguente rappresentazione:

_images/pc.svg

Seguirà una fase di test per verificare se i requisiti hanno qualche problema.

Superata la fase di test andiamo in refinement. Ad esempio decidendo di gestire i depositi tramite due buffer a singola capacità.

PC: concurrent specification

Per un raffinamento con sistemi concorrenti, ipotizziamo di avere in parallelo: il produttore, il gruppo dei due buffer, il consumatore. Quindi sarà:

\[PC_{conc,2} = Prod \parallel_{\{ deposit \}} (Buff \parallel Buff) \parallel_{\{ withdraw \}} Cons\]

In questo modello, il produttore esegue deposito e diviene nuovamente produttore:

\[Prod = deposit \cdot Prod\]

Un buffer esegue un deposito, dopo di che deve eseguire un prelievo per poi divenire nuovamente buffer:

\[Buff = deposit \cdot withdraw \cdot Buff\]

Il consumatore esegue il prelievo e poi diviene nuovamente consumatore:

\[Cons = withdraw \cdot Cons\]

Analizzando funzionalmente il comportamento dei due modelli, sequenziale e concorrente, è possibile notare che sono bisimilarmente equivalenti.

L’equivalenza in questione può essere verificata anche formalmente, ad esempio utilizzando il tool Edinburgh Concurrency Workbench, o il Concurrency WorkBench of the New Century (CWB-NC).

Ad esempio, utilizzando il CWB-NC, possiamo scrivere la specifica come segue:

***********************************************************************
 * ProducerConsumer requirements: PC
 *    3 states: PC02, PC12, PC22, with 0 / 1 / 2 data of max 2 data
***********************************************************************
set Act = {deposit, withdraw}
proc PC02 = deposit.PC12
proc PC12 = deposit.PC22 + 'withdraw.PC02
proc PC22 = 'withdraw.PC12

mentre possiamo scrivere la modellazione con due buffer paralleli monodimensionali così:

***********************************************************************
 * Buffer cell model: B
 *    cicle through in.'out.startagain; buffer is two cells in parallel
***********************************************************************
proc B = deposit.'withdraw.B
proc Buffer = (B | B)

un controllo di uguaglianza in bisimulazione di PC02 rispetto Buffer ci dice TRUE:

...> cwb-nc ccs
/// omissis
cwb-nc> load pc.ccs
/// omissis
cwb-nc> eq -S bisim PC02 Buffer
Building automaton...
States: 8
Transitions: 14
Done building automaton.
TRUE
/// omissis