Các Kiểu Phiên và Tính Đồng thời Có Kiểu

Các kiểu phiên là các kiểu hành vi mô tả giao thức giao tiếp trên một kênh, cho phép kiểm tra kiểu đảm bảo rằng các tiến trình đồng thời tương tác chính xác.

Definition

Kiểu phiên là một kiểu mô tả giao thức được tuân thủ bởi một kênh giao tiếp, thứ tự và các kiểu thông điệp được gửi và nhận, để một trình kiểm tra kiểu có thể đảm bảo các bên tham gia giao tiếp theo một giao thức được xác định rõ ràng.

Scope

Chủ đề này bao gồm các nguyên tắc kiểu cho tính đồng thời, đặc biệt là các kiểu phiên và các kiểu hành vi chỉ định trình tự và hình dạng của các thông điệp được trao đổi giữa các tiến trình giao tiếp. Nó bao gồm các kiểu phiên nhị phân và đa bên, tính đối ngẫu và sự phù hợp của giao thức, các đảm bảo về an toàn giao tiếp và không bế tắc, cũng như mối tương ứng giữa các kiểu phiên và logic tuyến tính.

Core questions

• Làm thế nào một kiểu có thể mô tả một giao thức giao tiếp qua một kênh?
• Tính đối ngẫu là gì, và làm thế nào nó đảm bảo hai điểm cuối đồng ý?
• An toàn giao tiếp và không bế tắc được đảm bảo bằng cách đánh kiểu như thế nào?
• Các kiểu phiên liên quan đến logic tuyến tính thông qua mối tương ứng Curry-Howard như thế nào?

Key theories

Các kiểu phiên nhị phân

Honda, Vasconcelos và Kubo đã giới thiệu các kiểu phiên và một nguyên tắc đối ngẫu cho giao tiếp có cấu trúc, đảm bảo rằng hai điểm cuối của một kênh tuân theo các giao thức bổ sung, tương thích.

Các kiểu phiên đa bên

Honda, Yoshida và Carbone đã tổng quát hóa các kiểu phiên cho nhiều bên tham gia thông qua một giao thức toàn cục được chiếu vào các kiểu cục bộ, đảm bảo tương tác an toàn giữa nhiều bên.

Các kiểu phiên như các mệnh đề tuyến tính

Caires và Pfenning đã thiết lập một mối tương ứng Curry-Howard giữa các kiểu phiên và logic tuyến tính trực giác, mang lại các đảm bảo mạnh mẽ như không bế tắc từ khả năng đánh kiểu.

Clinical relevance

Các kiểu phiên và kiểu hành vi mang lại các đảm bảo tĩnh về sự phù hợp của giao thức, an toàn giao tiếp và không bế tắc cho phần mềm đồng thời và phân tán, và chúng đã được tích hợp vào các phần mở rộng ngôn ngữ và thư viện. Chúng biến các lỗi giao thức mà nếu không sẽ xuất hiện trong thời gian chạy thành các lỗi kiểu trong thời gian biên dịch.

History

Các kiểu phiên xuất phát từ công trình về pi-calculus có kiểu, được Honda và các đồng nghiệp hình thức hóa cho các phiên nhị phân vào năm 1993-1998. Các kiểu phiên đa bên đã mở rộng lý thuyết cho nhiều bên tham gia vào năm 2008, và mối tương ứng logic năm 2010 của Caires và Pfenning đã kết nối các kiểu phiên với logic tuyến tính, thúc đẩy nghiên cứu tính đồng thời có kiểu không bế tắc và các công cụ thực tế.

Debates

Tính biểu cảm so với tính thực tiễn của việc đánh kiểu hành vi

Các nhà nghiên cứu tranh luận về mức độ phong phú của các hệ thống kiểu phiên, cân bằng giữa sức mạnh của các đảm bảo như không bế tắc và sự phù hợp của giao thức với gánh nặng chú thích và khó khăn tích hợp trong các ngôn ngữ chính thống.

Key figures

• Kohei Honda
• Nobuko Yoshida
• Marco Carbone
• Luís Caires
• Frank Pfenning

Seminal works

• honda1998
• honda2008
• caires2010

Frequently asked questions

Một kiểu phiên đảm bảo điều gì?

Một phiên được đánh kiểu tốt đảm bảo an toàn giao tiếp, nghĩa là mỗi thông điệp có kiểu mong đợi và các bên tuân theo giao thức đã thỏa thuận; các hệ thống phong phú hơn còn đảm bảo tiến trình hoặc không bế tắc.

Tính đối ngẫu trong các kiểu phiên là gì?

Tính đối ngẫu là mối quan hệ giữa hai điểm cuối của một kênh: bất cứ điều gì một điểm cuối gửi, điểm cuối kia phải nhận, và ngược lại, để hai giao thức cục bộ phù hợp với nhau thành một cuộc hội thoại mạch lạc.