Algoritmi - Esercizio di sincronizzazione..

Buongiorno, per la preparazione ad un esame universitario sto svolgendo alcuni esercizi di sincronizzazione. La traccia di uno di questi è la seguente:

Un servizio di pool-car ha a disposizione N automobili, ognuna assegnata ad una zona della città. Gli utenti del servizio si recano al punto di partenza e prenotano un posto sull'automobile per la zona desiderata. Ogni automobile ha a disposizione M posti. Una volta occupati gli M posti, il veicolo parte per la zona stabilita. Nel caso in cui sia trascorso un tempo T, a partire dalla prima prenotazione per una determinata zona, il veicolo parte per la zona assegnata. Nel caso in cui non ci siano posti disponibili su un veicolo, gli utenti in eccesso si mettono in attesa della prossima corsa per la zona desiderata.

La mia implementazione in uno pseudo-linguaggio è la seguente, e desidererei conoscere il vostro parere e gli eventuali (certi) errori di logica in essa:

// Dichiarazioni delle variabili e delle strutture dati condivise tra i processi. 

mutex: semaforo binario:= 1;
mutex1: semaforo binario:= 1;
tempo: int:= 10;

struct AUTO {
	cont_posti: int:= M;
 	posti: semaforo generico:= M;
	piena: semaforo binario:= 0;
} auto;
auto automobili[N];

PROCESSO UTENTE i:
	repeat 
		begin
			wait(mutex);  
			if(automobili[ 0 <= i <= N].cont_posti > 0) 
				// Nel caso in cui ci sono dei posti disponibili per quella vettura, allora l’utente 
				// se ne impossessa di uno. Inoltre decrementiamo il semaforo generico in modo
				// che quando questo arriva a 0, tutti gli altri utenti dovranno attendere su di 
				// esso per poter usufruire della vettura. 

				automobili[ 0 <= i <= N].cont_post—;
				wait(automobili[ 0 <= i <= N].posti);
			else 
				signal(mutex);
				wait(automobili[ 0 <= i <= N].posti);
			end if
			signal(mutex);
		end
	forever
FINE PROCESSO

PROCESSO AUTO j:
	repeat 
		begin 
			for (i to tempo) 
				if(automobili[ 0 <= i <= N].cont_posti < M-1 AND automobili[ 0 <= i <= N].cont_posti != 0) 
					sleep(tempo);
					signal(automobili[ 0 <= i <= N].piena);
					break;
				end if
			end for
			
			// Nel caso in cui l’auto venga schedulata dopo che tutti i posti sono stati presi, allora si deve 
			// segnalare che l’auto è piena e pronta a partire. 

			if(automobili[ 0 <= i <= N].cont_posti == 0)
				signal(automobili[ 0 <= i <= N].piena);
			end if

			wait(automobili[ 0 <= i <= N].piena);
			viaggia per un tempo Q qualsiasi;

			// Quando l’auto ritorna, allora deve essere svuotata e quindi le variabili precedenti ed i semafori 
			// devono essere riportati ai valori precedenti. 

			wait(mutex1);
			for(i to M)
				automobili[ 0 <= i <= N].cont_posti++;
				signal(automobili[ 0 <= i <= N].posti);
			end for
			signal(mutex1);
		end
	forever
FINE PROCESSO