Các Mô hình đồng thời và Phép tính tiến trình

Các mô hình đồng thời và phép tính tiến trình cung cấp các mô tả hình thức về cách các tiến trình độc lập thực thi, giao tiếp và đồng bộ hóa.

Definition

Phép tính tiến trình là một đại số hình thức để mô tả các hệ thống đồng thời dưới dạng các tiến trình giao tiếp, với các toán tử cho thành phần song song, giao tiếp và lựa chọn, cùng với các tương đương xác định khi hai tiến trình hoạt động giống nhau.

Scope

Chủ đề này bao gồm các mô hình đại số của tính toán đồng thời: CSP của Hoare và CCS của Milner, phép tính pi cho các tiến trình di động có cấu trúc liên kết giao tiếp thay đổi, và mô hình actor của việc truyền thông điệp không đồng bộ. Nó đề cập đến các nguyên thủy giao tiếp và đồng bộ hóa, các tương đương hành vi như bisimulation, và sự tương phản giữa đồng thời bộ nhớ chia sẻ và truyền thông điệp.

Core questions

• Làm thế nào có thể mô tả đại số các tiến trình giao tiếp đồng thời?
• Khi nào hai tiến trình đồng thời tương đương về mặt hành vi?
• Truyền thông điệp so sánh như thế nào với đồng thời bộ nhớ chia sẻ?
• Các cấu trúc giao tiếp động được mô hình hóa như thế nào, như trong phép tính pi?

Key theories

Các tiến trình tuần tự giao tiếp (CSP)

CSP của Hoare mô hình hóa tính đồng thời thông qua các tiến trình đồng bộ hóa trên các sự kiện giao tiếp chia sẻ, cung cấp nền tảng cho các ngôn ngữ truyền thông điệp và một lý thuyết về tinh chỉnh tiến trình.

CCS và bisimulation

Phép tính các hệ thống giao tiếp của Milner đưa ra một đại số các tiến trình với một khái niệm chính xác về tương đương hành vi, bisimulation, để lý luận về khi nào các tiến trình có thể hoán đổi cho nhau.

Phép tính pi

Milner, Parrow và Walker đã mở rộng các phép tính tiến trình sang tính di động, cho phép các kênh giao tiếp tự chúng được truyền dưới dạng thông điệp để cấu trúc kết nối phát triển một cách động.

Clinical relevance

Các phép tính tiến trình và mô hình actor làm nền tảng cho việc thiết kế các ngôn ngữ và khung công tác đồng thời và phân tán được xây dựng trên truyền thông điệp, và chúng cung cấp các công cụ hình thức để đặc tả và xác minh các giao thức. Bisimulation và tinh chỉnh đưa ra các tiêu chí chính xác cho hành vi đồng thời đúng đắn.

History

Lý thuyết đồng thời đã trưởng thành vào cuối những năm 1970 với CSP của Hoare và CCS của Milner, trong khi mô hình actor của Hewitt (1973) đưa ra một giải pháp thay thế truyền thông điệp không đồng bộ. Phép tính pi vào năm 1992 đã nắm bắt được tính di động của tiến trình. Các phép tính này đã ảnh hưởng đến các ngôn ngữ truyền thông điệp và thư viện đồng thời và vẫn là nền tảng cho việc xác minh giao thức.

Debates

Bộ nhớ chia sẻ so với truyền thông điệp

Một câu hỏi thiết kế cơ bản là liệu tính đồng thời nên được tổ chức xung quanh trạng thái có thể thay đổi được chia sẻ với đồng bộ hóa hay xung quanh các tiến trình cô lập trao đổi thông điệp, với các phép tính tiến trình và mô hình actor ủng hộ phương án sau.

Key figures

• C. A. R. Hoare
• Robin Milner
• Carl Hewitt
• Joachim Parrow
• David Walker

Seminal works

• hoare1978
• milner1989
• milner1992
• hewitt1973

Frequently asked questions

Bisimulation là gì?

Bisimulation là một tương đương trên các tiến trình mà giữ khi mỗi tiến trình có thể khớp với các bước quan sát được của tiến trình kia vô thời hạn, hình thức hóa ý tưởng rằng hai tiến trình đồng thời thể hiện cùng một hành vi.

Phép tính pi bổ sung gì so với các phép tính trước đó?

Phép tính pi mô hình hóa tính di động bằng cách cho phép các kênh giao tiếp được gửi dưới dạng thông điệp, do đó cấu trúc liên kết về việc ai có thể nói chuyện với ai có thể thay đổi trong quá trình thực thi, nắm bắt các hệ thống động và có thể cấu hình lại.