Ảnh chụp toàn cầu và trạng thái

Một ảnh chụp toàn cầu ghi lại một cái nhìn nhất quán về trạng thái của một tính toán phân tán—trạng thái cục bộ của mỗi tiến trình cộng với các thông điệp đang truyền—mà không làm đóng băng hệ thống.

Definition

Một trạng thái toàn cầu nhất quán là một tập hợp các trạng thái tiến trình cục bộ và nội dung kênh tương ứng với một lát cắt nhất quán—trong đó, đối với mỗi lần nhận thông điệp được ghi lại, việc gửi tương ứng cũng được ghi lại—để trạng thái đó có thể phát sinh trong quá trình tính toán mặc dù không có thời điểm toàn cầu nào được quan sát.

Scope

Chủ đề này bao gồm khái niệm về trạng thái toàn cầu nhất quán và lát cắt định nghĩa nó, thuật toán ảnh chụp dựa trên đánh dấu của Chandy-Lamport và các giả định của nó (kênh FIFO, phân phối đáng tin cậy), và ứng dụng của ảnh chụp để phát hiện thuộc tính ổn định như phát hiện kết thúc và tắc nghẽn, cũng như để kiểm tra và phục hồi phân tán.

Core questions

• Điều gì làm cho một trạng thái toàn cầu được ghi lại trở nên nhất quán thay vì không thể?
• Làm thế nào có thể ghi lại một trạng thái như vậy trong khi tính toán vẫn tiếp tục chạy?
• Làm thế nào để phát hiện các thuộc tính ổn định như kết thúc và tắc nghẽn từ các ảnh chụp?

Key theories

Các lát cắt nhất quán

Một trạng thái toàn cầu tương ứng với một lát cắt qua các chuỗi sự kiện của các tiến trình; lát cắt là nhất quán chính xác khi nó được đóng dưới quan hệ xảy ra trước, đảm bảo không có thông điệp nào được nhận trước khi nó được gửi trong trạng thái được ghi lại.

Thuật toán ảnh chụp Chandy-Lamport

Một trình khởi tạo ghi lại trạng thái của nó và gửi một đánh dấu trên mỗi kênh đi; mỗi tiến trình, khi lần đầu tiên nhận được một đánh dấu, ghi lại trạng thái của nó và sau đó ghi lại các thông điệp đến trên các kênh khác cho đến khi các đánh dấu của chúng đến, ghi lại nội dung kênh.

Phát hiện thuộc tính ổn định

Bởi vì các ảnh chụp ghi lại một trạng thái mà hệ thống có thể đã ở trong đó, bất kỳ thuộc tính ổn định nào (một thuộc tính vẫn đúng khi nó đã đúng, chẳng hạn như kết thúc hoặc tắc nghẽn) được phát hiện trong một ảnh chụp thực sự đúng, làm cho các ảnh chụp trở thành một công cụ phát hiện tổng quát.

Clinical relevance

Các thuật toán ảnh chụp cung cấp khả năng kiểm tra/khởi động lại phân tán để phục hồi lỗi, bao gồm cả việc chụp ảnh không đồng bộ được sử dụng bởi các công cụ xử lý luồng hiện đại để cung cấp đảm bảo chính xác một lần, cũng như phát hiện tắc nghẽn và kết thúc trong các tính toán chạy dài.

History

Thuật toán của Chandy và Lamport năm 1985 đã đưa ra phương pháp thực tế đầu tiên để ghi lại một trạng thái toàn cầu nhất quán mà không dừng hệ thống; Mattern và những người khác đã tổng quát hóa lý thuyết lát cắt cơ bản, và kỹ thuật này sau đó trở thành nền tảng cho xử lý luồng chịu lỗi.

Key figures

• K. Mani Chandy
• Leslie Lamport
• Friedemann Mattern

Seminal works

• chandy1985
• mattern1989
• lynch1996

Frequently asked questions

Việc chụp ảnh có yêu cầu tạm dừng hệ thống không?

Không. Thuật toán Chandy-Lamport ghi lại một trạng thái toàn cầu nhất quán trong khi tính toán vẫn tiếp tục, bằng cách truyền các đánh dấu dọc theo các kênh; trạng thái được ghi lại là một trạng thái mà hệ thống có thể đã ở trong đó, mặc dù nó không bao giờ bị dừng hoàn toàn.