เครื่องหมายอัฒภาคที่รั่ว
Author
Venue
เอกสารการประชุมวิชาการ ACM ด้านภาษาการเขียนโปรแกรม ประจำปี 2021
Abstract
ตรรกะและอรรถาธิบายของโปรแกรมเล่าเรื่องราวที่น่าพึงพอใจเกี่ยวกับการประมวลผลแบบลำดับ: เมื่อดำเนินการ (S1; S2) เราจะดำเนินการ S1 ก่อนแล้วจึงดำเนินการ S2 อย่างไรก็ตาม เพื่อปรับปรุงประสิทธิภาพ โปรเซสเซอร์จะดำเนินการคำสั่งโดยไม่เรียงลำดับ และคอมไพเลอร์จะจัดลำดับโปรแกรมใหม่ให้มากขึ้นอีกตามความเหมาะสม โดยออกแบบแล้ว ระบบแบบเธรดเดียวไม่สามารถสังเกตเห็นการจัดลำดับใหม่เหล่านี้ได้ แต่ระบบแบบหลายเธรดสามารถทำได้ ซึ่งทำให้เรื่องราวไม่น่าพึงพอใจเท่าเดิม ความพยายามอย่างเป็นทางการในการทำความเข้าใจความยุ่งเหยิงที่เกิดขึ้นเรียกว่า "โมเดลหน่วยความจำแบบผ่อนคลาย" (relaxed memory model) โมเดลก่อนหน้านั้นไม่สามารถจัดการกับการประกอบลำดับโดยตรง หรือจำกัดตัวประมวลผลและคอมไพเลอร์มากเกินไป หรืออนุญาตให้เกิดพฤติกรรมที่ไร้สาระและไม่สามารถสังเกตได้ในทางปฏิบัติ เพื่อสนับสนุนการประกอบลำดับในขณะที่มุ่งเป้าไปที่ฮาร์ดแวร์สมัยใหม่ เราเสริมแนวทางตามเหตุการณ์มาตรฐานด้วยเงื่อนไขก่อนและกลุ่มของตัวแปลงนิพจน์เชิงตรรกะ เมื่อคำนวณความหมายของ (S1;S2) ตัวแปลงคำกริยาที่ใช้กับเงื่อนไขก่อนเหตุการณ์ e จาก S2 จะถูกเลือกตามชุดของเหตุการณ์ใน S1 ที่ e ขึ้นอยู่ด้วย เราใช้แนวทางนี้กับแบบจำลองหน่วยความจำที่มีอยู่สองแบบ
