แบบจำลองการทำงานพร้อมกันและแคลคูลัสกระบวนการ

แบบจำลองการทำงานพร้อมกันและแคลคูลัสกระบวนการให้คำอธิบายที่เป็นทางการว่ากระบวนการอิสระทำงาน สื่อสาร และประสานงานกันอย่างไร

Definition

แคลคูลัสกระบวนการคือพีชคณิตเชิงรูปนัยสำหรับอธิบายระบบที่ทำงานพร้อมกันในฐานะกระบวนการสื่อสาร โดยมีตัวดำเนินการสำหรับการประกอบแบบขนาน การสื่อสาร และการเลือก และความเท่าเทียมกันที่กำหนดว่าเมื่อใดที่กระบวนการสองกระบวนการมีพฤติกรรมเหมือนกัน

Scope

หัวข้อนี้ครอบคลุมแบบจำลองเชิงพีชคณิตของการคำนวณแบบพร้อมกัน: CSP ของ Hoare และ CCS ของ Milner, pi-calculus สำหรับกระบวนการเคลื่อนที่ที่โครงสร้างการสื่อสารเปลี่ยนแปลงได้, และ actor model ของการส่งข้อความแบบอะซิงโครนัส โดยกล่าวถึงหลักการพื้นฐานของการสื่อสารและการประสานงาน, ความเท่าเทียมกันทางพฤติกรรม เช่น bisimulation, และความแตกต่างระหว่างการทำงานพร้อมกันแบบหน่วยความจำร่วมกับการส่งข้อความ

Core questions

• กระบวนการสื่อสารที่ทำงานพร้อมกันสามารถอธิบายในเชิงพีชคณิตได้อย่างไร?
• เมื่อใดที่กระบวนการที่ทำงานพร้อมกันสองกระบวนการมีความเท่าเทียมกันทางพฤติกรรม?
• การส่งข้อความเปรียบเทียบกับการทำงานพร้อมกันแบบหน่วยความจำร่วมได้อย่างไร?
• โครงสร้างการสื่อสารแบบไดนามิกถูกจำลองอย่างไร เช่นใน pi-calculus?

Key theories

Communicating Sequential Processes (CSP)

CSP ของ Hoare จำลองการทำงานพร้อมกันผ่านกระบวนการที่ประสานงานกันบนเหตุการณ์การสื่อสารร่วมกัน ซึ่งเป็นรากฐานสำหรับภาษาการส่งข้อความและทฤษฎีการปรับปรุงกระบวนการ

CCS และ bisimulation

Calculus of Communicating Systems ของ Milner ให้พีชคณิตของกระบวนการที่มีแนวคิดที่แม่นยำของความเท่าเทียมกันทางพฤติกรรม, bisimulation, สำหรับการให้เหตุผลว่าเมื่อใดที่กระบวนการสามารถใช้แทนกันได้

The pi-calculus

Milner, Parrow และ Walker ได้ขยายแคลคูลัสกระบวนการไปสู่การเคลื่อนที่ โดยอนุญาตให้ช่องทางการสื่อสารเองถูกส่งผ่านเป็นข้อความ เพื่อให้โครงสร้างการเชื่อมต่อพัฒนาไปอย่างไดนามิก

Clinical relevance

แคลคูลัสกระบวนการและ actor model เป็นรากฐานของการออกแบบภาษาและเฟรมเวิร์กแบบพร้อมกันและแบบกระจายที่สร้างขึ้นบนการส่งข้อความ และเป็นเครื่องมือที่เป็นทางการสำหรับการระบุและตรวจสอบโปรโตคอล Bisimulation และ refinement ให้เกณฑ์ที่แม่นยำสำหรับพฤติกรรมที่ถูกต้องของการทำงานพร้อมกัน

History

ทฤษฎีการทำงานพร้อมกันพัฒนาขึ้นในช่วงปลายทศวรรษ 1970 ด้วย CSP ของ Hoare และ CCS ของ Milner ในขณะที่ actor model ของ Hewitt (1973) เสนอทางเลือกในการส่งข้อความแบบอะซิงโครนัส Pi-calculus ในปี 1992 ได้รวบรวมการเคลื่อนที่ของกระบวนการ แคลคูลัสเหล่านี้มีอิทธิพลต่อภาษาการส่งข้อความและไลบรารีการทำงานพร้อมกัน และยังคงเป็นรากฐานสำหรับการตรวจสอบโปรโตคอล

Debates

หน่วยความจำร่วมกับการส่งข้อความ

คำถามการออกแบบพื้นฐานคือว่าการทำงานพร้อมกันควรจัดระเบียบโดยใช้สถานะที่เปลี่ยนแปลงได้ร่วมกันกับการประสานงาน หรือโดยใช้กระบวนการที่แยกจากกันซึ่งแลกเปลี่ยนข้อความ โดยแคลคูลัสกระบวนการและ actor model สนับสนุนแนวคิดหลัง

Key figures

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

Seminal works

• hoare1978
• milner1989
• milner1992
• hewitt1973

Frequently asked questions

Bisimulation คืออะไร?

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

Pi-calculus เพิ่มอะไรจากแคลคูลัสก่อนหน้านี้?

Pi-calculus จำลองการเคลื่อนที่โดยอนุญาตให้ช่องทางการสื่อสารถูกส่งเป็นข้อความ ดังนั้นโครงสร้างของว่าใครสามารถพูดคุยกับใครได้สามารถเปลี่ยนแปลงได้ในระหว่างการดำเนินการ ซึ่งจับภาพระบบแบบไดนามิกและสามารถกำหนดค่าใหม่ได้