ประเภทเซสชันและการทำงานพร้อมกันแบบระบุประเภท

ประเภทเซสชัน (session types) เป็นประเภทเชิงพฤติกรรมที่อธิบายระเบียบวิธีสื่อสารผ่านช่องทาง ทำให้การตรวจสอบประเภท (type checking) สามารถรับประกันได้ว่ากระบวนการที่ทำงานพร้อมกันมีการโต้ตอบกันอย่างถูกต้อง

Definition

ประเภทเซสชันคือประเภทที่อธิบายระเบียบวิธีที่ช่องทางการสื่อสารปฏิบัติตาม ลำดับและประเภทของข้อความที่ส่งและรับ เพื่อให้ตัวตรวจสอบประเภทสามารถมั่นใจได้ว่าผู้เข้าร่วมสื่อสารตามระเบียบวิธีที่กำหนดไว้อย่างชัดเจน

Scope

หัวข้อนี้ครอบคลุมระเบียบวินัยด้านประเภทสำหรับการทำงานพร้อมกัน โดยเฉพาะประเภทเซสชันและประเภทเชิงพฤติกรรมที่ระบุลำดับและรูปแบบของข้อความที่แลกเปลี่ยนระหว่างกระบวนการสื่อสาร ซึ่งรวมถึงประเภทเซสชันแบบไบนารีและแบบหลายฝ่าย ความเป็นคู่ (duality) และการปฏิบัติตามระเบียบวิธี (protocol conformance) การรับประกันความปลอดภัยในการสื่อสารและการปลอดภาวะชะงักงัน (deadlock freedom) และความสอดคล้องกันระหว่างประเภทเซสชันกับตรรกะเชิงเส้น (linear logic)

Core questions

• ประเภทสามารถอธิบายระเบียบวิธีสื่อสารผ่านช่องทางได้อย่างไร?
• ความเป็นคู่คืออะไร และรับประกันได้อย่างไรว่าปลายทางทั้งสองเห็นพ้องต้องกัน?
• ความปลอดภัยในการสื่อสารและการปลอดภาวะชะงักงันได้รับการรับประกันโดยการระบุประเภทได้อย่างไร?
• ประเภทเซสชันเกี่ยวข้องกับตรรกะเชิงเส้นผ่านความสอดคล้องของ Curry-Howard อย่างไร?

Key theories

ประเภทเซสชันแบบไบนารี

Honda, Vasconcelos และ Kubo ได้นำเสนอประเภทเซสชันและระเบียบวินัยความเป็นคู่สำหรับการสื่อสารที่มีโครงสร้าง เพื่อให้มั่นใจว่าปลายทางทั้งสองของช่องทางปฏิบัติตามระเบียบวิธีที่เสริมกันและเข้ากันได้

ประเภทเซสชันแบบหลายฝ่าย

Honda, Yoshida และ Carbone ได้ขยายประเภทเซสชันไปยังผู้เข้าร่วมหลายคนผ่านระเบียบวิธีสากล (global protocol) ที่ถูกฉายไปยังประเภทท้องถิ่น (local types) ซึ่งรับประกันการโต้ตอบที่ปลอดภัยระหว่างหลายฝ่าย

ประเภทเซสชันในฐานะประพจน์เชิงเส้น

Caires และ Pfenning ได้สร้างความสอดคล้องของ Curry-Howard ระหว่างประเภทเซสชันและตรรกะเชิงเส้นแบบสัญชาตญาณ (intuitionistic linear logic) ซึ่งให้การรับประกันที่แข็งแกร่ง เช่น การปลอดภาวะชะงักงันจากการระบุประเภท (typability)

Clinical relevance

ประเภทเซสชันและประเภทเชิงพฤติกรรมนำมาซึ่งการรับประกันแบบสถิต (static guarantees) ในเรื่องการปฏิบัติตามระเบียบวิธี ความปลอดภัยในการสื่อสาร และการปลอดภาวะชะงักงันสำหรับซอฟต์แวร์ที่ทำงานพร้อมกันและแบบกระจาย และได้ถูกรวมเข้ากับการขยายภาษาและไลบรารีต่างๆ สิ่งเหล่านี้เปลี่ยนข้อผิดพลาดของระเบียบวิธีที่อาจเกิดขึ้นในขณะรันไทม์ให้กลายเป็นข้อผิดพลาดประเภทในขณะคอมไพล์

History

ประเภทเซสชันเกิดขึ้นจากการทำงานเกี่ยวกับ pi-calculus แบบระบุประเภท (typed pi-calculus) ซึ่งได้รับการจัดรูปแบบสำหรับเซสชันแบบไบนารีโดย Honda และเพื่อนร่วมงานในช่วงปี 1993-1998 ประเภทเซสชันแบบหลายฝ่ายได้ขยายทฤษฎีไปยังผู้เข้าร่วมหลายคนในปี 2008 และความสอดคล้องเชิงตรรกะของ Caires และ Pfenning ในปี 2010 ได้เชื่อมโยงประเภทเซสชันเข้ากับตรรกะเชิงเส้น ซึ่งกระตุ้นให้เกิดการวิจัยการทำงานพร้อมกันแบบระบุประเภทที่ปลอดภาวะชะงักงันและเครื่องมือเชิงปฏิบัติ

Debates

ความสามารถในการแสดงออกเทียบกับการใช้งานได้จริงของการระบุประเภทเชิงพฤติกรรม

นักวิจัยถกเถียงกันว่าระบบประเภทเซสชันควรมีความสมบูรณ์เพียงใด โดยต้องสร้างสมดุลระหว่างความแข็งแกร่งของการรับประกัน เช่น การปลอดภาวะชะงักงันและการปฏิบัติตามระเบียบวิธี กับภาระในการใส่คำอธิบายประกอบและความยากลำบากในการรวมเข้ากับภาษาหลัก

Key figures

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

Seminal works

• honda1998
• honda2008
• caires2010

Frequently asked questions

ประเภทเซสชันรับประกันอะไรบ้าง?

เซสชันที่ระบุประเภทอย่างถูกต้องรับประกันความปลอดภัยในการสื่อสาร ซึ่งหมายความว่าแต่ละข้อความมีประเภทที่คาดไว้และฝ่ายต่างๆ ปฏิบัติตามระเบียบวิธีที่ตกลงกันไว้ ระบบที่ซับซ้อนยิ่งขึ้นยังรับประกันความคืบหน้าหรือการปลอดภาวะชะงักงันเพิ่มเติม

ความเป็นคู่ในประเภทเซสชันคืออะไร?

ความเป็นคู่คือความสัมพันธ์ระหว่างปลายทางทั้งสองของช่องทาง: สิ่งใดก็ตามที่ปลายทางหนึ่งส่ง อีกปลายทางหนึ่งจะต้องรับ และในทางกลับกัน เพื่อให้ระเบียบวิธีท้องถิ่นทั้งสองเข้ากันได้ดีในการสนทนาที่สอดคล้องกัน