L'assignment chiede due versioni concorrenti del gioco Poool: (v1) multithreading con soli platform thread e monitor implementati da noi, (v2) una variante task-based sull'Executor Framework. Il codice sta in assignments/assignment-01/src/pcd/sketch01 ed è organizzato in modo che le due versioni siano due strategie intercambiabili dietro la stessa interfaccia: così fisica e ordine delle fasi restano identici e il confronto di performance è onesto.
Board possiede lo stato (palline, buche, punteggi) e l'ordine delle fasi di un frame; una PhysicsStrategy decide solo come e su quali thread eseguire le fasi parallelizzabili. Il frame è una pipeline di sei passi:
Grid, Cell): una riduzione su input disgiunto, parallelizzabile;Intorno alla pipeline c'è un main loop (Sketch01) in stile game loop: svuota in modo non bloccante due Buffer<PlayerAction> (input tastiera dalla EDT via ViewFrame, input del bot dal thread BotBehavior), applica gli impulsi, chiama board.updateState(dt), aggiorna la ViewModel (monitor con snapshot copiati) e fa il render sincrono con la EDT tramite il monitor RenderSynch. La mappa lastHitBy in Board attribuisce il punto a chi ha colpito per ultimo la pallina imbucata.
ThreadPoolStrategy)Un insieme fisso di worker (CollisionDetector, thread collision-worker-i) viene avviato una volta e vive per tutta la partita. A ogni frame il chiamante partiziona le celle della griglia in modo statico (cell.x mod workerCount), consegna a ogni worker un CollisionTask attraverso il suo Buffer dedicato, e si blocca su un monitor Barrier finché tutti hanno riportato. I monitor sono tutti nostri, costruiti su synchronized/wait/notifyAll:
Buffer<T> — coda produttore/consumatore con next() bloccante (worker) e poll() non bloccante (game loop);Barrier<T> — rendezvous a round che fa tre cose: blocca il chiamante finché tutte le parti hanno riportato, aggrega i risultati parziali, e scarta segnali marcati con un round passato (guardia di generazione);RenderSynch — sincronizza il game loop con la EDT sul frame renderizzato.In v1 solo la detection è parallela; integrate e buildGrid restano sul thread chiamante. Due limiti sono documentati nel codice stesso e sono il motivo di v2: la partizione statica fa aspettare tutti al barrier quando un worker pesca la striscia densa della board, e il Barrier aggrega in ordine di completamento, quindi l'ordine delle coppie (e della successiva risoluzione) varia tra esecuzioni.
ExecutorStrategy)Un Executors.newFixedThreadPool(poolSize) con ThreadFactory propria (thread physics-i, daemon). Il task è il corpo del lavoro, non più il loop perpetuo del worker: ogni fase produce una lista di Callable e awaitAll li consegna a invokeAll, che è insieme il rendezvous e il punto di aggregazione — il Barrier sparisce. Rispetto a v1:
chunksPerThread): un thread che finisce presto prende un altro chunk invece di aspettare;Future.get(), non da un monitor nostro.Completano il quadro SequentialStrategy (baseline per lo speedup) e gli helper condivisi di Grid — dove newGrid() ritorna apposta una LinkedHashMap, per rendere l'ordine di iterazione delle celle indipendente da come è stato spartito il lavoro.
PhysicsBenchmark — sweep di tutte le strategie sulla board massive (4500 palline, MassiveBoardConf), con warmup e trial multipli; riporta tempo medio di frame e speedup rispetto al sequenziale, variando pool size e chunk per thread;StrategyEquivalence — controllo di correttezza: stessa board, stessi frame, confronto di ogni coordinata finale con la baseline. Atteso: executor IDENTICAL, platform-threads può differire negli ultimi bit (ordine di completamento, non una race);jpf/TestBarrier + jpf/UnsafeBarrier + verify-jpf.sh — model checking JPF del monitor Barrier (2 parti, 2 round) e di una copia deliberatamente rotta che dimostra che il setup rileva davvero i difetti.Il codice delle due versioni richieste c'è ed è funzionante, ma il lavoro è in progress: la cartella doc/ con report.pdf (analisi, design, reti di Petri, numeri di benchmark) non esiste ancora, e nel package restano CalculateGrid e Loc, residui di un tentativo precedente di parallelizzare la griglia, oggi non referenziati da nessuno.
La consegna chiede costrutti di alto livello con implementazione propria: i tre monitor (Buffer, Barrier, RenderSynch) usano il pattern canonico Java — synchronized, wait() dentro un while sulla condizione, notifyAll() — cioè la disciplina signal-and-continue dei monitor Java (Cap. 7 — Monitor e variabili condizione). Il while è obbligatorio: tra il notify e la ripresa il lock va riacquisito e nel frattempo la condizione può essere tornata falsa (risvegli spuri, altri consumatori).
Tastiera (EDT) e bot producono PlayerAction su due Buffer; il game loop consuma. È lo schema produttore/consumatore classico (Cap. 5 — Semafori e problemi classici), ma con una variante importante: il game loop non può bloccarsi, quindi usa poll() (ritorna Optional.empty() a coda vuota), mentre i worker di v1 usano next() bloccante. Il monitor è anche il punto di pubblicazione sicura: gli impulsi vengono applicati alla pallina solo dal thread del main loop, dopo il passaggio dal buffer.
Il Barrier di v1 è un rendezvous: il main aspetta che tutti i worker abbiano riportato. La guardia di generazione (signalDone(gen, ...) ignora round passati) protegge il barrier — che è un oggetto longevo, riusato ogni frame — da un report tardivo di un round precedente. La correttezza del protocollo (niente perso, niente duplicato, il main non resta bloccato) è verificata con JPF (Cap. 11 — Verifica formale e model checking). Sui rischi di attese circolari e di segnali persi: Cap. 6 — Deadlock.
In v1 il loop perpetuo del worker («prendi dal mio inbox, calcola, riporta») è politica di esecuzione scritta a mano dentro il worker; in v2 l'unità di lavoro è solo il calcolo e la politica è del pool (Cap. 10 — Concorrenza in Java). invokeAll sostituisce in una chiamata il rendezvous e l'aggregazione del Barrier, e la visibilità dei risultati è garantita dall'happens-before di Future.get() (le azioni nel task happen-before il ritiro del risultato) invece che dal nostro synchronized.
// ExecutorStrategy.awaitAll: rendezvous + aggregazione in una chiamata
List<Future<T>> futures = pool.invokeAll(tasks);
for (Future<T> future : futures) { // ordine di sottomissione, non di completamento
results.add(future.get()); // happens-before: vedo tutte le scritture del task
}
V1 ha necessariamente un chunk per thread (la partizione è l'inbox del thread); v2 sottomette poolSize × chunksPerThread chunk che si accodano, così chi finisce presto continua a lavorare. Con una distribuzione delle palline non uniforme e che cambia ogni frame, nessuna partizione statica resta buona a lungo — e su core eterogenei (P-core/E-core) le partizioni uguali garantiscono che i core lenti tengano fermo ogni rendezvous. Decidere cosa parallelizzare (scritture disgiunte, riduzioni, letture pure) e cosa no è un'analisi delle dipendenze tra i passi, cioè data decomposition più vincoli d'ordine: Cap. 8 — Progettare programmi concorrenti.
Lo speedup ha senso solo se il programma veloce calcola la stessa cosa: per questo v2 fonde i parziali in ordine di sottomissione e Grid.newGrid() usa una LinkedHashMap (l'ordine di iterazione delle celle determina l'ordine di risoluzione del pass 4, che è order-dependent). StrategyEquivalence trasforma questa proprietà in un check eseguibile. Distinzione da saper difendere: il non determinismo di v1 non è una race — ogni accesso è sincronizzato — ma dipendenza del risultato dall'ordine di completamento (Cap. 3 — Correttezza: safety, liveness, fairness, LTL).
ViewFrame.render() chiede il repaint() e poi si blocca su RenderSynch.waitForFrameRendered(nf) finché la EDT non ha davvero dipinto: rendering sincrono per evitare race tra paint e aggiornamento della view model. In più ViewModel è un monitor che copia snapshot immutabili (BallViewInfo record), così la EDT non tocca mai lo stato vivo di Board (Cap. 7 — Monitor e variabili condizione).
verify-jpf.sh lancia due run: il Barrier vero (atteso: nessun errore su tutti gli interleaving) e UnsafeBarrier, copia con una sola parola tolta (synchronized su signalDone). Il bug seminato è la lost update su ++count: nessuna assert scatta, il programma semplicemente non avanza — JPF lo trova come deadlock: raggiunge uno stato in cui nessun thread può proseguire. «Il main prima o poi riparte» è una proprietà di liveness, che JPF controlla cercando uno stato bloccato raggiungibile; nessuna asserzione sugli stati la rileva (Cap. 11 — Verifica formale e model checking).
Su questo assignment Ricci ha chiesto: come è strutturata la soluzione e quali ne sono gli aspetti concorrenti principali (§1–2); come avete scelto il numero di thread e se cambiarlo cambiava le prestazioni; come coordinate le fasi tra componenti attivi e passivi; se il buffer è bounded o unbounded; quali prove di correttezza avete fatto, come avete usato JPF e se le proprietà verificate sono di safety o di liveness. Ha anche annunciato la domanda «come capite che i task sono finiti?». Tutte hanno una risposta qui sotto.
Java implementa i monitor con disciplina signal-and-continue: chi viene notificato non entra subito, deve riacquisire il lock, e nel frattempo la condizione può essere tornata falsa (un altro consumatore ha svuotato la coda, o è arrivato un risveglio spurio). Il while ricontrolla la condizione a ogni risveglio; con un if si procederebbe su una condizione non più vera. Riferimento nel codice: Buffer.next() e Barrier.await().
Attivi: il thread del main loop (Sketch01), i worker collision-worker-i di v1 (in v2 i thread physics-i del pool), il thread del bot (BotBehavior) e la EDT di Swing. Passivi: i monitor Buffer, Barrier, RenderSynch, ViewModel, e Board, il cui stato è confinato al main loop. Il main loop esegue le fasi nell'ordine fissato da Board; per ogni fase parallela distribuisce il lavoro (un Buffer per worker in v1, invokeAll in v2) e attende il rendezvous (Barrier o invokeAll) prima della fase successiva: uno schema master-worker ripetuto a ogni frame (Cap. 8 — Progettare programmi concorrenti).
L'insieme dei task di una fase è fissato prima di sottometterli e il loro numero è noto. In v1 il Barrier conta i report fino al numero di worker e solo allora sblocca il main; in v2 invokeAll ritorna solo quando tutti i Future della lista sono completati. Non serve quindi un meccanismo di terminazione per lavoro generato dinamicamente.
La fisica è CPU-bound (quasi nessuna attesa: W/C ≈ 0), quindi la regola Nthread = Ncpu · Ucpu · (1 + W/C) dà circa un thread per core, Ncpu + 1 per coprire le pause occasionali (Cap. 10 — Concorrenza in Java). Il valore va poi confermato misurando: PhysicsBenchmark varia il numero di worker e, per l'executor, i chunk per thread. Oltre il numero di core lo speedup non cresce più e il residuo seriale (pass 4–6) fissa il tetto. I numeri concreti (valore scelto nel gioco, speedup misurati sulla propria macchina) vanno portati dal report.
Unbounded: nessuna back-pressure, la coda potrebbe crescere se il produttore corresse più del consumatore. Qui i produttori sono strutturalmente lenti (tastiera, bot con sleep fino a 1,5 s) e il game loop svuota tutto con poll() a ogni frame, quindi la coda resta corta. Un bounded buffer (il caso canonico di Cap. 5) bloccherebbe il produttore a coda piena: per la EDT sarebbe un difetto, perché congelerebbe l'interfaccia.
Il Barrier è un oggetto longevo riusato a ogni frame. Senza guardia, un report in ritardo di un round precedente (es. un worker interrotto o lento) verrebbe contato nel round corrente: count salirebbe due volte per lo stesso worker e il main potrebbe sbloccarsi con risultati mancanti o duplicati. signalDone(gen, ...) confronta il round dichiarato con quello corrente e scarta i segnali stantii. In v2 la guardia non serve più: invokeAll non riusa nulla tra i round, quindi la situazione è irrappresentabile invece che difesa.
Ogni monitor ha un solo lock e nessun metodo di un monitor chiama un altro monitor tenendo il proprio lock: manca la condizione di hold-and-wait tra lock (una delle quattro condizioni di Coffman), quindi non può formarsi un'attesa circolare. L'unico blocco è su condizioni (wait, che rilascia il lock) sempre accoppiate a un notifyAll raggiungibile: il barrier si sblocca quando l'ultimo worker riporta, il buffer quando qualcuno produce. Il rischio residuo — un worker muore e il barrier aspetta per sempre — è gestito da interrupt in close(); il protocollo del barrier è verificato con il deadlock detector di JPF (Cap. 6).
Le coppie rilevate condividono palline: (A,B) e (B,C) scrivono entrambe B. Risolverle in parallelo sarebbe una race; mettere un lock per pallina eliminerebbe la race ma non l'order-dependence — il risultato fisico dipende dall'ordine di risoluzione — e il lavoro per coppia è troppo piccolo per ammortizzare il locking. Stessa analisi per il pass 5 (ogni iterazione scrive playerBall e botBall). La divisione è documentata nel commento di PhysicsStrategy e di Board.updateState.
Per il Java Memory Model, le azioni di un task in un ExecutorService happen-before il ritiro del suo risultato via Future.get(). In awaitAll ogni risultato passa da future.get(), quindi il main vede tutte le scritture del task (posizioni delle palline incluse, anche nei task Callable<Void> di integrate). In v1 la stessa garanzia la dava il nostro monitor: signalDone e await sono synchronized sullo stesso lock, e unlock/lock stabiliscono l'happens-before.
Tre cose misurabili e una concettuale. (1) Bilanciamento: chunk disaccoppiati dai thread (chunksPerThread), quindi niente attese al barrier per la partizione statica sfortunata. (2) Copertura: v2 parallelizza anche integrate e buildGrid, abbassando il residuo seriale che per Amdahl limita lo speedup di v1. (3) Determinismo: merge in ordine di sottomissione, quindi output identico al sequenziale (verificato da StrategyEquivalence). Concettuale: il task è il corpo del lavoro, la politica di esecuzione è del pool — la separazione che l'Executor Framework esiste per fornire.
No, e la distinzione va fatta con precisione. Ogni accesso condiviso in v1 è correttamente sincronizzato (nessun data race, JPF non trova errori sul barrier). Ma il Barrier aggrega i parziali in ordine di completamento, che varia tra run; il pass 4 risolve le collisioni in quell'ordine, e la risoluzione è order-dependent, quindi le posizioni finali possono differire negli ultimi bit. È un non determinismo di scheduling sul risultato, non un accesso non sincronizzato — ed è esattamente la proprietà che rende il pass 4 non parallelizzabile.
Correttezza: StrategyEquivalence (stesso risultato della baseline sequenziale) e JPF sul Barrier (domanda successiva). Prestazioni: PhysicsBenchmark sulla board massive (4500 palline), warmup di almeno 20 frame, trial multipli, media del tempo di frame; sweep sul numero di worker (1, 2, 4, …, core disponibili) e, per l'executor, sui chunk per thread (1, 2, 4). Atteso: speedup sublineare — Amdahl con i pass 4–6 seriali fissa il tetto; v1 sotto v2 a parità di worker perché parallelizza solo la detection e paga la partizione statica; l'effetto dei chunk visibile soprattutto con distribuzioni dense non uniformi e su core eterogenei.
JPF esplora tutti gli interleaving del monitor Barrier con 2 parti e 2 round (jpf/TestBarrier). Proprietà di safety, con assert: nessun contributo perso o duplicato, la generazione avanza una volta per round. Proprietà di liveness, col deadlock detector di JPF: il main non resta bloccato per sempre. La scala minima è scelta: con 1 parte non ci sono interleaving tra worker, con 1 round la guardia di generazione è irraggiungibile. UnsafeBarrier toglie synchronized da signalDone: la lost update su ++count fa sì che notifyAll non parta mai e await() penda per sempre — un fallimento di liveness che nessuna assert vede e che l'esecuzione normale quasi mai riproduce. Serve a dimostrare che «no errors detected» sul barrier vero significa qualcosa: lo stesso setup rileva un difetto reale (Cap. 11).
Per confinamento: gli impulsi vengono applicati solo dal thread del main loop, che li estrae dai due Buffer con poll() prima di updateState. EDT e bot non toccano mai la pallina: producono PlayerAction (enum immutabile) nel buffer, che essendo un monitor è anche il punto di pubblicazione sicura. Lo stato vivo di Board è confinato al main thread; verso la EDT viaggiano solo gli snapshot immutabili copiati dentro il monitor ViewModel.
La detection itera grid.keySet() e l'ordine delle coppie rilevate è l'ordine con cui il pass 4 — order-dependent — le risolve. Con HashMap l'ordine di iterazione dipende dalla storia di inserimento della tabella: costruire la griglia con una scansione sequenziale o fondendo N mappe parziali produce ordini diversi, quindi simulazioni misurabilmente diverse. LinkedHashMap fissa l'ordine a «prima apparizione scandendo le palline in ordine», indipendente da come è stato spartito il lavoro, a costo trascurabile. È il tassello che, insieme al merge in ordine di sottomissione, rende v2 identica alla baseline.
Cooperativamente, via interrupt. A fine partita (o uscita dal loop) Sketch01 nel finally chiama board.shutdown() — che delega a strategy.close(): in v1 interrupt e join di ogni worker (il worker esce dal next() bloccante rilanciando lo stato di interrupt), in v2 pool.shutdownNow() più awaitTermination — e poi interrompe e joina il thread del bot, che esce dalla sleep. detect() restituisce null se il chiamante viene interrotto a metà rendezvous e updateState abbandona il frame senza risolvere collisioni parziali.
Non del tutto: assume un solo thread in await() (il main). È await a resettare contatore, lista e generazione; se due thread aspettassero, il primo risveglio consumerebbe i risultati e resetterebbe il round sotto i piedi del secondo. Inoltre le parti non aspettano tra loro (i worker riportano e proseguono): è più un rendezvous con aggregazione che una barriera simmetrica. L'assunzione è legittima nel design — il protocollo ha un solo coordinatore per costruzione — ma va dichiarata; il test JPF modella esattamente questo schema, non quello generale.
Il report non c'è ancora. La consegna richiede doc/report.pdf con analisi del problema, design (anche con reti di Petri), test di performance e verifica. Il materiale esiste sparso nei commenti di PhysicsStrategy, ExecutorStrategy, Grid e negli harness (PhysicsBenchmark, StrategyEquivalence, verify-jpf.sh), ma va consolidato: servono i numeri di benchmark effettivi della propria macchina (media, speedup per worker/chunk) e almeno una rete di Petri del protocollo main/worker/barrier di v1 (Cap. 9 — Formalismi visuali: reti di Petri e statechart).
CalculateGrid e Loc non sono referenziati da nessuna strategia — residui di un tentativo precedente sul bucketing. Da rimuovere prima della consegna, o all'orale sembrano parte del design.invokeAll.dt misurato; niente sleep verso un target fps. Sulla board minimal consuma un core intero per nulla. Facile da difendere come scelta di semplicità, ma va riconosciuto.ViewFrame fa System.exit(-1) su windowClosing, bypassando shutdown()/interrupt. Incoerente con la terminazione cooperativa curata altrove.Buffer e RenderSynch non hanno harness; se all'orale chiedono «perché proprio il barrier?», la risposta è che è il monitor col protocollo più ricco (round, generazioni, aggregazione) e l'unico con un fallimento non banale da esibire — ma la scelta va argomentata, non subita. Nota pratica: verify-jpf.sh richiede JDK 11 per jpf-core mentre il progetto compila a 17; sapere il perché (jpf-core non builda su 17+).(1) La distinzione race vs order-dependence, con StrategyEquivalence come prova; (2) il perché di ogni singola parola di Barrier.await() — while, notifyAll e non notify, il reset dentro await; (3) la lettura dei numeri del benchmark alla luce di Amdahl (residuo seriale = pass 4–6); (4) la run JPF di UnsafeBarrier: saper raccontare l'interleaving che perde l'incremento senza guardare il codice.