Лінеаризовність
У паралельному програмуванні операція (або набір операцій) є лінеаризованою, якщо вона складається з упорядкованого списку подій виклику та відповіді (події), які можна розширити додаванням відповіді таким чином, що:
- Розширений список можна повторно виразити як послідовну історію (можна серіалізувати).
- Ця послідовна історія є підмножиною вихідного нерозширеного списку.
Неформально це означає, що немодифікований список подій можна лінеаризувати тоді й лише тоді, коли його виклики можна серіалізувати, але деякі відповіді послідовного розкладу ще не повернулися.[1]
У паралельній системі процеси можуть отримати доступ до спільного об’єкта одночасно. Оскільки кілька процесів звертаються до одного об’єкта, може виникнути ситуація, коли один процес звертається до об’єкта, поки інший змінює його вміст. Перетворення системи на лінеаризацію є одним із рішень цієї проблеми. У системі, що лінеаризується, хоча операції на спільному об’єкті накладаються, кожна операція виглядає миттєво. Можливість лінеаризації — це сувора умова правильності, яка обмежує можливі результати, коли до об’єкта одночасно звертаються кілька процесів. Це властивість безпеки, яка гарантує, що операції не завершаться неочікуваним або непередбачуваним чином. Якщо система є лінеаризованою, це дозволяє програмісту міркувати про систему.[2]
- ↑ Herlihy, Maurice P.; Wing, Jeannette M. (1990). Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems. 12 (3): 463—492. CiteSeerX 10.1.1.142.5315. doi:10.1145/78969.78972.
- ↑ Shavit, Nir; Taubenfel, Gadi (2016). The Computability of Relaxed Data Structures: Queues and Stacks as Examples (PDF). Distributed Computing. 29 (5): 396—407. doi:10.1007/s00446-016-0272-0.