next up previous contents index
Next: Lebendigkeit Up: 2.3.2 Programmeigenschaften Previous: 2.3.2 Programmeigenschaften

Sicherheit

  Der Beweis von deadlock-Freiheit kann durch Techniken erfolgen, wie sie z.B. in dem Buch von Andrews beschrieben sind. Wenn etwa BAD ein Prädikat bezeichnet, das einen deadlock charakterisiert, so könnte man zeigen, daß

für alle Bedingungen (Preconditions) in allen Programmteilen c: c tex2html_wrap_inline2270 tex2html_wrap_inline2272 BAD.
Womit dann bewiesen wäre, daß die Bedingung BAD nicht eintreten könnte, das Programm also deadlock frei wäre.

Eine andere Technik benutzt eine Invariante  I, die in allen Programmteilen gilt und zeigt

I tex2html_wrap_inline2270 tex2html_wrap_inline2272 BAD.
Wodurch dann ebenfalls sichergestellt ist, daß BAD nicht eintreten kann.

Ist das nicht möglich, kann eventuell noch durch sogenanntes exclusion of configurations   (u.U. durch explizites await) sichergestellt werden, daß keine Interferenz auftritt.



parallel@rz.uni-mannheim.de
Mon Okt 28 14:38:25 PST 1996