Compiti ed esercitazioni VERIFICATO

Compito del 4 settembre 2019+soluzioni

Università degli studi di Firenze informatica 2019
98 visualizzazioni
6 download
Nessun voto ancora
Condividi: WhatsApp Telegram

Di cosa parla

Riassunto AI · si legge in un minuto

Questo documento esamina concetti di programmazione concorrente attraverso esercizi pratici. Tratta la formalizzazione LTL e la dimostrazione per induzione computazionale di invarianti per l'algoritmo di Dekker. Include la costruzione di diagrammi di stato per programmi basati su semafori per analizzare proprietà di liveness. Vengono presentate soluzioni per il problema dei Filosofi a Cena (due filosofi) garantendo assenza di deadlock e starvation. Viene inoltre progettato un monitor per un incrocio stradale con gestione della precedenza tramite condition variables, con un'implementazione Java che utilizza ReentrantLock e Condition, e una discussione sui potenziali scenari di starvation.
Leggi il riassunto completo
  • 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.

Riassunto generato con l'intelligenza artificiale a partire dagli appunti. Come lo facciamo

Anteprima pagina 1 — Compito del 4 settembre 2019+soluzioni

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

Studia questi appunti con l'AI

Riassunto e domande d'esame sono gratis: chiedili e ti mandiamo un'email quando sono pronti.

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

Simula l'esame con domande costruite su questi appunti.

Altri appunti di PROGRAMMAZIONE CONCORRENTE

Condividi questi appunti

WhatsApp Telegram