Also entweder hab ich was verpasst oder mein Gedächtnis ist ein Sieb, aber kann mir bitte irgendjemand genau erklären, wie ich mit xspin oder spin die Korrektheit eines Programmes beweise?
Versteht mich nicht falsch... ich war bei der "Einführung in Spin" (den Aufwand in Ehren, aber die dazugehörigen Folien sind im Nachhinein alles andere als eine Hilfe), in jeder Vorlesung und in jeder Übung und meine Gruppe hat sich bisher schon ausgiebig mit xspin beschäftigt - aber irgendwo will mir nicht 100%ig klar werden, wie ich vorzugehen habe.
Ok, den wechselseitigen Ausschluss zu zeigen, ist nicht weiter das Problem... aber bei der Verklemmungsfreiheit fängt es an... Reicht es, in jeden Prozess ein progress-Label zu packen und dann auf non-progress-cycles zu testen? Das dürfte doch eigentlich genügen, da das System ja nie zum Halt kommt, seh ich das richtig?
Und wie sieht es mit dem Verhungern aus? Bisher haben wir einen never-claim mit
Code: Alles auswählen
!((G F p1_in_critical_section) && (G F p2_in_critical_section))Also gilt Fairness als vorrausgesetzt?
Ich kann mir nicht vorstellen, dass meine Gruppe die einzige ist, die sich solche Fragen stellt... also wäre ich über eine detaillierte Antwort bezüglich des Verifikationsablaufs dankbar.
MfG
SM
