面對多核處理器技術的不斷革新,為充分地利用多核資源提升程序的性能,設計和實現(xiàn)高并發(fā)的數據結構變得越來越重要。為獲得 多的并發(fā)和 好的性能,程序開發(fā)者會盡可能地采用細粒度同步技術來實現(xiàn)并發(fā)數據結構。然而這些數據結構通常復雜靈巧、易出錯、可靠性難以保證。因此,形式化驗證并發(fā)數據結構對提高并發(fā)軟件的可靠性和安全性有著重要意義。可線性化是一一個主流的并 發(fā)數據結構安全性標準。本書針對并發(fā)數據結構可線性化標準及其驗證方法方面進行了深入研究。本書分析了可線性化標準的局限性,在此基礎上提出了強可線性化標準。本書致力于提供簡單易用的方法驗證并發(fā)數據結構的可線性化。