Compiti ed esercitazioni VERIFICATO

Compito del 4 settembre 2019+soluzioni

Università degli studi di Firenze informatica 2019
20 visualizzazioni
6 download
Nessun voto ancora
Condividi: WhatsApp Telegram
Anteprima pagina 1 — Compito del 4 settembre 2019+soluzioni

Stai vedendo l'anteprima delle prime pagine. Il file completo è gratis: registrati per leggerlo tutto.

Di cosa parla

  • Esercizio 1: Algoritmo di Dekker
    • Formalizzazione LTL dell'asserzione: "Se wantp è sempre vero e turn vale sempre 1, allora wantq diventa falso e lo rimane per sempre." Soluzione: □(want p ^ (turn = 1)) ⇒ ◇□¬wantq.
    • Dimostrazione per induzione computazionale dell'invariante: wantq ⇒ (q3..5 V q8..10). La dimostrazione verifica la verità nello stato iniziale e analizza le transizioni di stato che modificano o rendono falsa la premessa, garantendo la conclusione.
  • Esercizio 2: Diagramma degli Stati per Semafori
    • Costruzione del diagramma degli stati per un programma concorrente con due semafori (S e T).
    • Analisi della proprietà di liveness: "P entra infinite volte in p2". Il diagramma mostra che tutti i cicli includono p2, confermando la proprietà.
  • Esercizio 3: Problema dei Filosofi a Cena (2 Filosofi)
    • Soluzione basata su semafori per due filosofi, acquisendo le forchette in ordine (prima f0 poi f1).
    • Assenza di deadlock garantita dall'ordine di acquisizione. Starvation freedom è assicurata dal meccanismo di sblocco e disponibilità delle risorse.
  • Esercizio 4: Monitor per Incrocio Stradale
    • Implementazione di un monitor per regolare il traffico (NS o EO), con operazioni enterCrossing(dir) e leaveCrossing(dir).
    • Variabili chiave: P (direzione di precedenza), C (auto nell'incrocio), waitingCar[0..1] (condition variables).
    • enterCrossing attende se incrocio occupato o precedenza non per propria direzione.
    • leaveCrossing cambia precedenza se incrocio si svuota e ci sono auto in attesa nell'altra direzione.
    • Rischio di starvation: un flusso continuo in una direzione può impedire alle auto nell'altra di accedere indefinitamente.
  • Esercizio 5: Implementazione Java del Monitor per Incrocio
    • Implementazione in Java del monitor usando ReentrantLock e Condition.
    • Classe Crossing con variabili P, C, waiting (contatori auto in attesa) e waitPred (array di Condition).
    • enterCrossing attende sulla condizione waitPred[dir] se C>0 && P!=dir.
    • leaveCrossing, se incrocio vuoto e auto in attesa nell'altra direzione, cambia P e notifica (signalAll) su waitPred[1-dir].
    • Le considerazioni sulla starvation sono analoghe all'esercizio 4.

Questo appunto è gratis. Registrati in 30 secondi per leggere tutte le pagine e scaricarlo.

Altri appunti di PROGRAMMAZIONE CONCORRENTE

Condividi questi appunti

WhatsApp Telegram