Bộ nhớ đệm lười trong TLA

Distributed Computing - Tập 12 - Trang 151-174 - 1999
Peter Ladkin1, Leslie Lamport2, Bryan Olivier3, Denis Roegel4
1 Universität Bielefeld, Technische Fakultät, Postfach 10 01 31, D-33501 Bielefeld, Germany , , DE
2 Sytems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, USA (e-mail: [email protected]) , , US
3 Kattenburgergracht 17, Appt. E, NL-1018 KN Amsterdam, The Netherlands , , NL
4 LORIA, Campus Scientifique, B.P. 239, F-54506 Vandeouvre-les-Nancy Cedex, France , , FR

Tóm tắt

Chúng tôi giải quyết vấn đề do Gerth đề xuất, đó là xác minh rằng một phiên bản đơn giản hóa của thuật toán lưu trữ lười của Afek, Brown và Merritt là nhất quán theo thứ tự. Chúng tôi xác định thuật toán và tính nhất quán theo thứ tự trong TLA$^+$, một ngôn ngữ biên soạn chính thức dựa trên TLA (Logic Thời gian của Các hành động). Sau đó, chúng tôi mô tả cách xây dựng và kiểm tra một bằng chứng tính đúng đắn chính thức trong TLA.

Từ khóa


Thông tin
Thông tin xuất bản

Distributed Computing

Tập 12

151-174

Thông tin tác giả