Fragen zu Lab1

[yourmaninamsterdam]

was soll denn in die abgabe dann alles mit rein? alle asserts die uns so eingefallen sind? was ist mit weiteren ausgaben? haben uns noch einige prints eingebaut damit wir den code leichter testen konnten, aber das macht den code an sich unübersichtlicher.

wenn die asserts drin bleiben sollen: sollen die dann auch mit jedem N funktionieren?

Was genau in die Abgabe gehört, steht auf dem Aufgabenblatt. Bitte versucht, die Abgabe möglichst kompakt und übersichtlich zu halten. Das hat mehrere Vorteile (für alle Beteiligten):

• Kleinere (aber noch vollständige) Modelle sind bessere Modelle, weil ihre Angemessenheit für einen Dritten leichter zu beurteilen ist. Alle wesentlichen Aspekte der zu modellierenden Situation sollten sich im Modell wiederfinden; alle anderen Aspekte nicht.
• Eure Abgabe wird einfacher zu korrigieren. Das ist zum einen fair den Tutoren (sie müssen sich nicht durch unnötig lange Lösungen quälen) und euren Mitstudenten gegenüber (die Tutoren können gleich viel Zeit ins Korrigieren investieren). Zum anderen ermöglicht es ein schnelles und gutes Feedback für euch.
• Es ist im Allgemeinen besser, Dokumente, die für andere Leute zur Durchsicht, Korrektur, etc. bestimmt sind, auf das Nötige zu beschränken, nicht nur in FGdI3-Labs. Das vereinfacht die Kommunikation zwischen dem Erzeuger des Dokuments und dem Empfänger.

[yourmaninamsterdam]

Noch zu den Asserts: Lasst bitte auch nur die asserts drin, die ihr für die Verifikation braucht und nicht "alle, die euch so eingefallen sind". Ich nehme an, es reicht, wenn das Programm mit N = 5 funktioniert. Aber da kann euch Nathan eher was zu sagen.

[dominique.metz]

Darf ein Philosoph eine Gabel nehmen und danach sie wieder zurücklegen, ohne dazwischen eine zweite Gabel aufzunehmen und zu essen?

[slashafk]

Stand schon ein Stückchen weiter oben

Kann der Philosoph denn mit einer Gabel in der Hand denken?

Um auf die zugrundelegende Frage zu antworten: Natürlich kann es sein, dass ein Philosoph eine Gabel hält und auf die andere warten muss.

[dominique.metz]

Vielen Dank für die Antwort, aber sie beantwortet nicht ganz meine Frage.
Dass ein Philosoph nicht vom Denken abgehalten werden darf, wenn er nur eine Gabel in der Hand hält (also die Ausführung des Prozesses wird geblockt, bis "seine" zweite Gabel wieder frei ist) ist mir klar. Aber darf er, wenn er sieht, dass seine zweite Gabel nicht frei ist, sich dazu entscheiden, seine bereits aufgehobene Gabel wieder hinzulegen? Oder denkt er solange weiter mit einer Gabel in der Hand, bis seine zweite verfügbar ist, ohne die erste hinzulegen und ggf. wieder aufzunehmen?

[Nathan Wasser]

Werden die Gabeln genauso zufällig und nicht glechizeitig wieder zurückgelegt, wie sie aufgehoben wurden?

Die Philosophen dürfen nach dem Essen die Gabeln so zurücklegen wie ihr das wollt.

Darf ein Philosoph eine Gabel nehmen und danach sie wieder zurücklegen, ohne dazwischen eine zweite Gabel aufzunehmen und zu essen?

Nein, wenn er eine genommen hat, will er die andere auch nehmen. (Selbst wenn er sie zurücklegen dürfte, löst das alleine das Problem nicht. Überlegt wie ihr den Deadlock vermeiden könnt, nicht wie ihr aus der Deadlock Situation doch irgendwie wieder rauskommt.)

wenn die asserts drin bleiben sollen: sollen die dann auch mit jedem N funktionieren?

Es reicht, wenn das Problem für N=5 gelöst ist. (Obwohl es eigentlich ohne Weiteres für jedes andere N dann auch funktionieren sollte... Aber falls nicht, N=5 reicht.)

[sven.lohrmann]

Nein, wenn er eine genommen hat, will er die andere auch nehmen. (Selbst wenn er sie zurücklegen dürfte, löst das alleine das Problem nicht. Überlegt wie ihr den Deadlock vermeiden könnt, nicht wie ihr aus der Deadlock Situation doch irgendwie wieder rauskommt.)

Das heißt dann aber wieder, dass man den Philosophen vorschreiben muss wie sie handeln sollen, um den Deadlock von vornherein zu vermeiden. In den vorherigen Post wurde jedoch gesagt das wir den Philosophen nicht vorschreiben sollen wie sie zu handeln haben, oder seh ich das jetzt falsch?

[yourmaninamsterdam]

Das heißt dann aber wieder, dass man den Philosophen vorschreiben muss wie sie handeln sollen, um den Deadlock von vornherein zu vermeiden. In den vorherigen Post wurde jedoch gesagt das wir den Philosophen nicht vorschreiben sollen wie sie zu handeln haben, oder seh ich das jetzt falsch?

Wenn du den Philosophenprozess programmierst, schreibst du natürlich im gewissen Sinne vor, wie ein Philosoph agiert. Das ist selbstverständlich auch in Ordnung. Wie soll das denn sonst gehen? Es geht lediglich darum, dass keine übergeordnete Instanz die Philosophen kontrollieren soll, z. B. ein Prozess der sagt: "Jetzt isst Philosoph 1, die anderen denken. Jetzt iss Philosoph 2, die anderen denken! ..." oder irgendwelche ähnlichen Arrangements.

[sven.lohrmann]

Noch zu den Asserts: Lasst bitte auch nur die asserts drin, die ihr für die Verifikation braucht und nicht "alle, die euch so eingefallen sind". Ich nehme an, es reicht, wenn das Programm mit N = 5 funktioniert. Aber da kann euch Nathan eher was zu sagen.

Was ist eigentlich, wenn sich die Korrektheit schon aus den IF-Statements ergibt? Sollen wir dennoch asserts einfügen (die hätten dann den selben Inhalt) oder diese weglassen (in dem Fall hätte ich bei meiner Lösung keine asserts mit drin)?

[yourmaninamsterdam]

Was ist eigentlich, wenn sich die Korrektheit schon aus den IF-Statements ergibt?

Die Frage deutet darauf hin, dass du den Zweck der Übung nicht verstanden hast. Als Faustregel kann man sagen, dass sich nie Korrektheit aus if-Statements ergibt. Wenn in deinem Programm natürlich Dinge stehen wie

Code: Alles auswählen

byte x = 0;
if
  :: (x > 0) -> assert(x > 0)
fi

dann kann das schon sein, dass if und assert das gleiche bedeuten.

Im Allgemeinen kann man aber aus einer Programmausführung aber nicht auf die Korrektheit des Programms schließen. Insbesondere nicht, weil es (im Gegensatz zu meinem Codeschnipsel) in der Regel gemeinsame Variablen zwischen Prozessen gibt und die Anzahl möglicher Programmabläufe mit verschiedenen if-Branches und Interleaving so schnell zunimmt, dass du nicht mehr Korrektheit einfach behaupten kannst. Bei einer Verifikation beweist du die Korrektheit des Modells im Bezug auf die Spezifikation (hier z.B. gegeben durch asserts). Dieser Beweis gilt für alle Programmausführungen. Dazu ist es natürlich nicht nur wichtig, ein korrektes Modell zu erzeugen, sondern auch, sinnvolle Eigenschaften für die Verifikation zu spezifizieren.

Sollte es tatsächlich so sein, dass alle deine asserts genau gleichbedeutend zu deinen ifs sind, dann solltest du nochmal überprüfen, ob du die richtigen Eigenschaften überprüfst.

[sven.lohrmann]

Als Faustregel kann man sagen, dass sich nie Korrektheit aus if-Statements ergibt.

Das ist mir schon klar. In deinem gewählten Beispiel ist der assert auch wichtig, da er ja nach der Auswertung des Guards in einen anderen Prozess "springen" kann.

Meine Frage bezog sich aber auf so ein Konstrukt:

Code: Alles auswählen

atomic {
if
  :: (x > 0) -> assert(x > 0)
fi
}

in dem Fall wird interleaving ja vermieden und somit kann im Statement nur x > 0 sein.

[yourmaninamsterdam]

In meinem Fall ist es gewissermaßen auch so. Zwar kann es zwischen der Auswertung des Guards und des Asserts zu Interleaving kommen, die Variable x ist aber lokal, sodass es zu keiner Änderung kommen sollte.

Aber das ist im Grunde auch egal, denn ich überprüfe da einfach keine sonderlich entscheidende Eigenschaft. Interessant sind eher Eigenschaften wie "es passiert nie, dass ..." oder "die Invariante ... gilt immer". Was ich da aber habe ist, "nachdem ich heraugefunden habe, dass x > 0, ist x > 0". Ist natürlich nicht falsch, aber auch nicht sonderlich spannend.

Über atomic-Blöcke kann man natürlich viel mehr solcher Situationen provozieren. Man sollte aber sparsam mit den Blöcken umgehen und nur in sinnvollem Umfang (wie z. B. "atomic test-and-set") verwenden. Du kannst ja sonst einfach einen atomic-Block um die komplette Implementierung des Prozesses setzen. Da lassen sich bestimmt auch viele Eigenschaften zeigen, aber das hilft dir ja nix, denn das Modell ist nicht gut.

Man muss hier dazu sagen, dass die Sache mit den Philosophen als Beispiel nicht besonders realitätsnah ist. Im Hinterkopf sollte man aber behalten, dass es eine Modellierungsübung ist. Nämlich eine Übung, sinnvoll zu modellieren. Wenn es nicht um einen akademischen Fall mit irgendwelchen Philosophen und Gabeln ginge, sondern um die Modellierung echter nebenläufiger Systeme (z. B. im Rahmen eines Schlüsselaustauschs o. ä.), könntest du auch nicht einfach alles mögliche atomic machen.

[sven.lohrmann]

Über atomic-Blöcke kann man natürlich viel mehr solcher Situationen provozieren. Man sollte aber sparsam mit den Blöcken umgehen und nur in sinnvollem Umfang (wie z. B. "atomic test-and-set") verwenden. Du kannst ja sonst einfach einen atomic-Block um die komplette Implementierung des Prozesses setzen. Da lassen sich bestimmt auch viele Eigenschaften zeigen, aber das hilft dir ja nix, denn das Modell ist nicht gut.

Dann ist die Übungsaufgabe aber nicht sonderlich gut gewählt. Denn genau das bietet sich hier an (zwar nicht der komplette Prozess, aber doch ein Großteil davon) und in der Aufgabenstellung war nur gefordert, dass wir den atomic Block nicht benutzen dürfen, um beide Gabeln auf ein mal aufzunehmen.

[yourmaninamsterdam]

Ich persönlich bin auch ein Fan von anderen Aufgaben, aber man muss es mit der Komplexität auch nicht gleich zu Beginn übertreiben, oder? Benutz doch einfach dein Wissen aus der Vorlesung und die Modellierungselemente aus der zweiten Übung, um ein kompaktes und übersichtliches Modell für den Sachverhalt zu erstellen und zu verifizieren. Wenn alles in einem atomic-Block steht und deine Asserts nur die Bedingung des Guards eines if wiedergeben, dann ist das weder ein gutes Modell, noch gute Eigenschaften, noch richtet sich das nach den bislang in der Vorlesung und Übung behandelten Themen und Methoden.

[khaled]

Muss das philosophisches Problem für beliebige "NUM_PHIL"s funktionieren? oder reicht es wenn die Lösung für "NUM_PHIL" = 5 läuft?

Edit: ich habe die oben stehende Antwort überlesen.(hat sich geklärt)

Khalid