แบบจำลองภาวะพร้อมกันและหน่วยความจำ
แบบจำลองภาวะพร้อมกันและหน่วยความจำกำหนดโครงสร้างของโปรแกรมพร้อมกันและวิธีที่เธรดที่ทำงานร่วมกันสังเกตหน่วยความจำที่ใช้ร่วมกัน ซึ่งเป็นรากฐานสำหรับซอฟต์แวร์คู่ขนานที่ถูกต้อง
Definition
แบบจำลองภาวะพร้อมกันอธิบายว่าการคำนวณที่ทำงานอย่างอิสระถูกประกอบและสื่อสารกันอย่างไร ในขณะที่แบบจำลองหน่วยความจำระบุว่าค่าใดที่การอ่านอาจสังเกตได้เมื่อเธรดพร้อมกันเข้าถึงหน่วยความจำที่ใช้ร่วมกัน โดยกำหนดข้อตกลงระหว่างโปรแกรมเมอร์ ภาษา และฮาร์ดแวร์
Scope
ขอบเขตนี้ครอบคลุมภาษาและทฤษฎีของภาวะพร้อมกัน: แคลคูลัสกระบวนการและแบบจำลองภาวะพร้อมกันสำหรับการสื่อสารและการซิงโครไนซ์, แบบจำลองความสอดคล้องของหน่วยความจำที่ระบุลำดับที่อนุญาตของการดำเนินการหน่วยความจำ, กลไกการซิงโครไนซ์และการปลอดจากการแข่งขันข้อมูล (data-race freedom), และระบบประเภทสำหรับภาวะพร้อมกัน เช่น ประเภทเซสชัน (session types) ซึ่งจะกล่าวถึงว่าภาษาให้ความหมายกับโปรแกรมที่ทำงานพร้อมกันและใช้สถานะร่วมกันได้อย่างไร
Sub-topics
Core questions
- กระบวนการสื่อสารพร้อมกันสามารถสร้างแบบจำลองและให้เหตุผลได้อย่างไร?
- โปรแกรมอาจสังเกตลำดับการดำเนินการหน่วยความจำใดได้บ้าง?
- การปลอดจากการแข่งขันข้อมูล (data races) ได้รับการรับประกันหรือระบุไว้อย่างไร?
- ประเภทสามารถควบคุมการสื่อสารและป้องกันข้อผิดพลาดของภาวะพร้อมกันได้อย่างไร?
Key theories
- แคลคูลัสกระบวนการ
- CSP ของ Hoare และ CCS และ pi-calculus ของ Milner นำเสนอทฤษฎีพีชคณิตของกระบวนการพร้อมกันที่สื่อสารกัน โดยมีตัวดำเนินการสำหรับการประกอบและการซิงโครไนซ์ และแนวคิดของความสมมูลเชิงพฤติกรรม (behavioral equivalence) เช่น bisimulation
- ความสอดคล้องเชิงลำดับ
- Lamport ได้กำหนดความสอดคล้องเชิงลำดับว่าเป็นข้อกำหนดที่การดำเนินการแบบมัลติโปรเซสเซอร์ปรากฏเป็นบางส่วนของการสลับการดำเนินการของแต่ละโปรเซสเซอร์ตามลำดับโปรแกรม ซึ่งเป็นพื้นฐานที่ใช้เปรียบเทียบแบบจำลองหน่วยความจำที่อ่อนกว่า
- แบบจำลองความสอดคล้องของหน่วยความจำ
- Adve และ Gharachorloo ได้จัดระบบสเปกตรัมของแบบจำลองความสอดคล้องของหน่วยความจำที่ใช้ร่วมกัน โดยอธิบายว่าลำดับที่ผ่อนคลายช่วยให้ประสิทธิภาพดีขึ้นได้อย่างไร ในขณะเดียวกันก็ทำให้การให้เหตุผลเกี่ยวกับโปรแกรมพร้อมกันซับซ้อนขึ้น
Clinical relevance
แบบจำลองหน่วยความจำได้กลายเป็นส่วนหนึ่งของข้อกำหนดภาษาหลัก (เช่นใน C++ และ Java) เนื่องจากฮาร์ดแวร์แบบมัลติคอร์ทำให้ลำดับที่ผ่อนคลายสามารถสังเกตได้ การทำความเข้าใจให้ถูกต้องเป็นสิ่งจำเป็นสำหรับซอฟต์แวร์พร้อมกันที่ถูกต้องและพกพาได้ แคลคูลัสกระบวนการและประเภทเซสชันเป็นข้อมูลในการออกแบบภาษาและโปรโตคอลการส่งข้อความ
History
ทฤษฎีภาวะพร้อมกันเติบโตมาจาก Petri nets และผลงานในปี 1970 ของ Hoare (CSP) และ Milner (CCS) ซึ่งต่อมาคือ pi-calculus สำหรับกระบวนการเคลื่อนที่ (mobile processes) Lamport ได้กำหนดความสอดคล้องเชิงลำดับ (sequential consistency) ในปี 1979; เมื่อฮาร์ดแวร์ที่ผ่อนคลายแพร่หลายมากขึ้น แบบจำลองหน่วยความจำจึงถูกกำหนดอย่างเป็นทางการสำหรับภาษาต่างๆ เช่น Java และ C++ ในช่วงปี 2000 และความหมายของหน่วยความจำแบบอ่อน (weak-memory semantics) กลายเป็นสาขาการวิจัยที่สำคัญ
Debates
- ความสอดคล้องของหน่วยความจำแบบเข้มงวดเทียบกับแบบผ่อนคลาย
- นักออกแบบแลกเปลี่ยนความเรียบง่ายที่เข้าใจง่ายของแบบจำลองที่เข้มงวด เช่น ความสอดคล้องเชิงลำดับ กับประสิทธิภาพของแบบจำลองที่ผ่อนคลายที่อนุญาตให้มีการจัดลำดับใหม่ ซึ่งทำให้การให้เหตุผลซับซ้อนขึ้นและต้องใช้ความหมายระดับภาษาที่ระมัดระวัง
Key figures
- C. A. R. Hoare
- Robin Milner
- Leslie Lamport
- Sarita Adve
Related topics
Seminal works
- hoare1978
- milner1989
- lamport1979
- adve1996
Frequently asked questions
- แบบจำลองหน่วยความจำคืออะไร?
- แบบจำลองหน่วยความจำคือข้อตกลงอย่างเป็นทางการที่ระบุว่าค่าใดที่การอ่านสามารถส่งคืนได้เมื่อหลายเธรดเข้าถึงหน่วยความจำที่ใช้ร่วมกัน โดยกำหนดว่าคอมไพเลอร์และฮาร์ดแวร์อาจทำการจัดลำดับใหม่ใดได้บ้าง และโปรแกรมเมอร์สามารถพึ่งพาอะไรได้บ้าง
- ความสอดคล้องเชิงลำดับคืออะไร?
- ความสอดคล้องเชิงลำดับกำหนดให้การดำเนินการพร้อมกันต้องทำงานเหมือนกับการสลับการดำเนินการของเธรดเพียงครั้งเดียวที่เคารพลําดับโปรแกรมของแต่ละเธรด ทำให้เป็นแบบจำลองหน่วยความจำที่เข้าใจง่ายที่สุด (แต่มักจะถูกผ่อนคลาย)