Verifikation Server-Drucker

[null]

Hallo,

in der letzten Übung sollten wir ein Computer-Drucker System implementieren. Dazu habe ich noch einmal eine Frage, weil ich mich ehrlich gesagt damit noch ein bisschen schwer tue.

Reicht es bereits aus, folgenden Code zu schreiben:

Code: Alles auswählen

bool print = false;

active [2] proctype Computer() {
	do
		:: print == false -> print = true; printf("Computer %d druckt\n", _pid); print = false;
	od
}

Es kommt eine wunderschöne unendlich andauerende Ausgabe, doch ich kann daraus nicht entnehmen, ob damit die Anforderung erfült ist. Ich dachte an ein "assert" - Statement, doch irgendwie finde ich den dazu rechten Platz im Code nicht.

Kann mir jemand sagen, ob der obige Code richtig ist und wie ich ihn verifziere?
Danke

[yourmaninamsterdam]

Lies doch mal das Material für die Vorlesung. Aus der Einführung kannst du entnehmen, warum deine Lösung nicht korrekt ist. Im Kapitel "Verifying with SPIN" kannst du nachlesen, wie du deine Modelle verifizieren kannst.

[null]

Hi

Sorry, ich wollte nicht, dass meine Fragen so herüberkommen, als ob ich mich nicht mit dem gestellten Material beschäftige. Ich tue dies regelmäßig, aber mir ist die Spin-Welt noch ein bisschen fern. Trotzdem habe ich mir die Materialien angeschaut und nun eine Lösung gefunden, die mit Spin (spin -a datei.pml; gcc -o pan pan.c; ./pan) verifiziert habe und 0 Fehler erhalte. Trotzdem habe ich noch ein paar Fragen:

Code: Alles auswählen

bool print = false;
int counter = 0;

active [2] proctype Computer() {
	atomic {
	if
	:: print == false -> 	
				print = true;
				counter++;
				printf("Computer %d druckt\n", _pid);
				counter--;
				assert(counter == 0);
				print = false;
	fi
	}

}

Mein Fehler war wohl, ohne den atomic-Block zu arbeiten. Ich verstehe jedoch nicht, warum dieser nötig ist. Meiner Ansicht nach kann auch ohne atomic-Block keine Verschränkung auftreten, weil der Guard true sein muss, damit gedruckt werden kann. Wo tritt genau die Verschränkung auf?

Vielen Dank für deine Hilfe

[yourmaninamsterdam]

Hier ein paar Hinweise:

• Interleaving kann nach jeder Anweisung stattfinden. Auch nach Guards, denn bei denen handelt es sich im Anweisungen.
• Dein assert scheint mir ungeeignet, die gewünschte Eigenschaft zu überprüfen. Was soll 'counter == 0' denn an der Stelle aussagen? Niemand druckt?
• Bedenke, dass du in Promela Systeme modellierst. Das heißt, du suchst nach einer vereinfachten, aber angemessenen Darstellung des Systems. Ein atomic-Block um komplette Prozesse zu setzen ist nie eine Lösung. Das würde ja bedeuten, dass Druckaufträge atomar sind.

[xquid]

Schau nochmal nach an welcher Stelle du etwas überprüfen willst.

[null]

Hallo,

nachdem die Lösung zu dieser Aufgabe erschienen ist, habe ich sir mir mal näher angeschaut. Dabei ist mir aber eine Frage aufgekommen. Es geht um diesen Teil:

Code: Alles auswählen

   :: atomic {  /* atomic test & set */
       printerStatus == free ->
       printerStatus = busy
       };
       printer++;
       printf("Sending pdf file to printer %d", _pid);
       printer--;
       printerStatus = free; 
  od

Die Überprüfung, ob der Drucker frei ist und die anschließende Setzung auf "busy" erfolgt innerhalb einer Anweisung, weil der entsprechende Code in einem atomic-Block steht. Mir ist jedoch nicht klar, warum die Variabel "print" niemals über 1 kommen kann.

Wo ist der Fehler im folgenden Szenario?

Drucker1 erteilt einen Auftrag. Die Variabel "printer" wird um 1 erhöht.
Drucker2 erteilt einen Auftrag. Er kommt nicht in den atomic-Block rein, weil das guad blockt und geht daher weiter. Damit wird "printer" um 1 erhöht.
Drucker1 gibt "Sending pdf file to printer" aus.
...


Nun ist die Variabel printer == 2. Warum kann das nicht sein? Das habe ich noch nicht so ganz verstanden!

Vielen Dank

[yourmaninamsterdam]

Er kommt nicht in den atomic-Block rein, weil das guad blockt und geht daher weiter.

Er geht nicht weiter, sondern blockiert, bis 'printerStatus == free' wahr wird.

[onbes]

Habe eine Frage zum Problem 6. Da soll man ja das gleiche Problem mit rendezvous channels lösen. Im Lösungsvorschlag steht nun, dass bei dieser Lösung ein Prozess verhungern (starvation) kann.

Der User1 könnte doch blocken und sobald "chanPrinter ! release" vom User0 gesendet wird und der Printer nicht mehr blockiert kann doch User1 sein "chanPrinter ! request" machen usw. oder etwa nicht?

Mir ist der Unterschied zw. der atomic Lösung zu der Channels Lösungung bezüglich starvation nicht klar.
Wo liegt mein Fehler?

[Nathan Wasser]

Natürlich existiert ein möglicher Run, indem jeder Klient mal zum Zug kommt. Es ist aber nicht ausgeschlossen, dass es einen Run gibt indem dies nicht der Fall ist. Genauso wie User1 blocken kann und sobald User0 den Channel freigibt zuschnappen kann, kann auch User0 einfach zuvor kommen und den Channel gleich wieder belegen.

Es gibt aber auch bei der atomic Test & Set Lösung keinen Schutz vor Starvation.