Logics and Models of Concurrent Systems (NATO Asi Series, Advanced Science Institutes Series, Series F, Computer and Systems Sciences, Vol 13)

Der Kooperationstest [Apt, Francez & de Roever] wurde ursprünglich entwickelt, um das proof-theoretische Analogon des verteilten Nachrichtenaustauschs zwischen disjunkten Prozessen zu erfassen, im Gegensatz zum Störfreiheitstest [Owicki & Gries], der das theoretische Nachrichtenanalog der gleichzeitigen Kommunikation mittels Interferenz durch gemeinsam gemeinsam genutzte Variablen darstellt. Einige Autoren ([Levin & Gries, Lamport & Schneider, Schlichting und Schneider]) betonen, dass beide Formen der Kommunikation theoretisch nur mit Interferenzfreiheit charakterisiert werden können, da Beweise für beide letztendlich einen Invarianzbeweis einer großen globalen Behauptung [Ashcroft], deren Invarianz gleichbedeutend ist Störungsfreiheit. Ich glaube jedoch, dass die charakteristische Natur des Kooperationstests in der Analyse dieser Autoren immer noch erhalten bleibt, da sich der Teil, der sich mit der Störungsfreiheit befasst, in ihrer Analyse auf die Aufrechterhaltung einer globalen Invariante spezialisiert ist, deren Ausdruck pro Prozess die Einführung von Hilfsvariablen erfordert, die nur in diesem Prozess aktualisiert werden, wodurch das Konzept der Unzusammenhängigkeit erhalten bleibt (im Gegensatz zu sharing), seit jetzt alle Variablen aus verschiedenen Prozessen sind disjunkt. Der Kooperationstest wurde angewendet, um die gleichzeitige Kommunikation zu charakterisieren, wie sie in Hoare Communicating Sequential Processes (CSP) [Hoare 2], Ichbiahs ADA [ARM] und Brinch Hansens Distributed Processes (DP) [Brinch Hansen] stattfindet. Diese Charakterisierung wurde durch Soliditäts- und Vollständigkeitsnachweise bestätigt [Apt 2, Gerth]. Wie beim Störfreiheitstest besteht diese Charakterisierung aus zwei Stufen, einer lokalen sequentiellen Stufe und einer globalen Stufe.