Abstraktion, Linearisierbarkeit

• nebenläufige Implementierung N einer Datenstrukturspezifikation P
• mit abstraction map a von N zu einer sequentiellen Implementierung S
• N heißt linearisierbar, falls es für jede nebenläufige Ausführung von N eine Folge von Linearisierungpunkten n₁, n₂,… gibt,

  so daß a(n₁), a(n₂),… eine P-korrekte Ausführung von S ist.

vgl. Shavit: Art of Multiproc. Prog. Sect. 9.3 Concurrent Reasoning