TITEL

Print-while-shutdown: gegarandeerd correcte berekening van een gedistribueerde systeemtoestand

SPREKER

Matthieu Helder, softwarearchitect, Océ

TAAL

Nederlands, sheets in het Engels

ABSTRACT

Océs Prismasync-printercontroller heeft onder meer de taak het energieverbruik van de multifunctional zo laag mogelijk te houden. Een van de strategieën die we hierbij toepassen, is het in slaap brengen van het systeem bij inactiviteit.

In de controller zijn meerdere subsystemen tegelijkertijd actief. Ze communiceren met elkaar door middel van berichten in Fifo-queues. Elk subsysteem kent een gedefinieerd aantal toestanden. Het systeem kan alleen gaan slapen als alle subsystemen in een specifieke state zijn.

De System State Manager (SSM) heeft onder meer als taak om het totale systeem in slaap te brengen en weer te wekken. Daartoe moet de SSM de systeemtoestand berekenen op basis van de individuele states van de subsystemen en deze subsystemen vertellen dat ze moeten gaan slapen. Een probleem dat hierbij speelt, is dat er racecondities kunnen optreden tussen messages (ze kruisen elkaar) met als gevolg een inconsistente systeemtoestand.

In deze lezing beschrijf ik hoe we dit probleem hebben gemodelleerd en presenteer ik een algoritme dat gegarandeerd de juiste systeemtoestand berekent. Tevens geef ik een bewijs van de correctheid van het algoritme. Hieruit volgen de voorwaarden waaraan de queues moeten voldoen.