Ante: แนวทางใหม่ที่ผสาน borrow checking กับ reference counting

 (verdagon.dev)
1 คะแนน โดย GN⁺ 4 시간 전 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Ante เป็นการออกแบบภาษาระบบที่ต้องการใช้ทั้งความยืดหยุ่นของ reference counting และความปลอดภัยของ borrow checking พร้อมหลีกเลี่ยง runtime panic แบบ Rust หรือ overhead จากการตรวจสอบ exclusive access ขณะรันไทม์แบบ Swift
  • กลไกหลักคือ shape-stability และ temporary uniq conversion ซึ่งทำให้สร้าง mutable borrow ให้กับฟิลด์ของค่าที่ถูกนับอ้างอิงได้อย่างปลอดภัย และจัดการค่าภายใน union เป็น uniq เฉพาะในขอบเขตที่จำกัด
  • Rc<RefCell<T>> ของ Rust หากใช้ผิดอาจเกิด panic ตอนรันไทม์ได้ ส่วน borrowing system ของ Swift มีการตรวจสอบ exclusive access ตอนรันไทม์ แต่ Ante พยายามจัดการบางกรณีด้วยกฎตอนคอมไพล์
  • ยังเป็นการออกแบบแบบ work-in-progress ที่นำไปใช้จริงแล้วเพียงบางส่วน และเนื่องจากต้องวิเคราะห์ชนิดแบบ recursive เพื่อตัดสินว่าสามารถไปถึงอ็อบเจกต์ใดอ็อบเจกต์หนึ่งได้หรือไม่ การเพิ่มฟิลด์จึงอาจกลายเป็น breaking API change ได้
  • แนวทางนี้ทำให้สมมติฐานที่ว่า shared mutable borrowing เป็นไปไม่ได้เสมออ่อนลง และกำลังขยายพื้นที่ข้อยกเว้นในการออกแบบความปลอดภัยหน่วยความจำร่วมกับเทคนิคอย่าง Vale, group borrowing และ Rust GhostCell

สิ่งที่ Ante ต้องการผสานเข้าด้วยกัน

  • Ante เป็นภาษาสำหรับ system programming ที่มุ่งเป็น Rust ที่เรียบง่ายกว่า พร้อม ความปลอดภัยของหน่วยความจำ และ ความปลอดภัยของเธรด
  • โมเดลพื้นฐานคือ ownership เดี่ยวและ borrow checking โดยค่าจะถูกวาง inline บน stack หรือภายใน struct/array ที่บรรจุมันอยู่
  • เมื่อต้องการให้ความเรียบง่ายมาก่อน สามารถเลือกใช้ reference counting ได้โดยใส่คีย์เวิร์ด shared ให้กับ type
  • ฟังก์ชัน balance ของ red-black tree ที่ใช้ shared type Color และ shared type RbTree t สั้นพอ ๆ กับตัวอย่าง Python และเล็กกว่าตัวอย่าง C++/Rust
  • ประเด็นหลักคือวิธีจัดการเมื่อ borrow ข้อมูลที่ถูกนับอ้างอิงแบบ mutable โดยไม่มีความเสี่ยง panic จาก borrow_mut() แบบ Rust หรือการตรวจสอบ exclusive access ตอนรันไทม์แบบ Swift
  • Ante ยังอยู่ในสถานะ work-in-progress โดยบางส่วนทำงานแล้ว บางส่วนยังเป็นทฤษฎี และการออกแบบยังเปลี่ยนแปลงอยู่

shape-stability และ mutable reference หลายตัว

  • shape-stability ของ Ante คือแนวคิดที่ว่า “reference ไปยังเป้าหมายที่มี stable shape จะยังใช้ได้เสมอ ไม่ว่าจะมีการเปลี่ยนแปลงใดเกิดขึ้นที่อื่น”
  • ด้วยแนวคิดนี้ จึงสามารถมี mutable borrow reference หลายตัวไปยัง struct เดียวกันได้พร้อมกัน
  • ในตัวอย่าง heal (healer: mut Entity) (target: mut Entity) สามารถเรียก self_heal เพื่อให้ตัวเองรักษาตัวเองได้โดยส่ง Entity เดียวกันเป็นอาร์กิวเมนต์ทั้งสองตัว
    • แม้ healer และ target จะชี้ไปยัง Entity เดียวกัน โค้ดนี้ก็ไม่สามารถทำลาย Entity ได้ ดังนั้น reference ทั้งสองจึงยังคงใช้ได้
  • mutable reference ไปยังตัว struct เอง ฟิลด์ของมัน และฟิลด์ย่อยของฟิลด์ ก็อาจได้รับอนุญาตพร้อมกันได้
    • แม้ใช้ ship: mut Spaceship และ engine_alias: mut Engine = ship.engine พร้อมกัน ก็ถือว่าระหว่างฟังก์ชันทำงาน ship และ engine ข้างในจะไม่ถูกทำลาย
  • Rust และ Swift ไม่อนุญาตรูปแบบที่มี &mut reference หลายตัวชี้ไปยังข้อมูลเดียวกันพร้อมกัน

mutable borrowing ฟิลด์ของค่าที่ถูก reference counted

  • ใน Ante หากเติม shared หน้าคำนิยาม type ชนิดนั้นจะถูก reference counted โดยอัตโนมัติ
  • ในตัวอย่าง shared mut type Spaceship ฟังก์ชัน launch ถือ Spaceship ที่เทียบได้กับ Rc ไว้ และส่ง mut ship.engine ให้ set_fuel
  • เนื่องจาก launch ยังคงรักษาอ็อบเจกต์ที่บรรจุอยู่คือ Spaceship ไว้ จึงตัดสินได้ว่าฟิลด์ engine ของมันยังมีชีวิตอยู่ด้วย
  • กฎทั่วไปคือสามารถสร้าง mut borrow reference ให้กับฟิลด์ของ type แบบ shared mut ได้เสมอ
    • แต่ไม่ได้หมายความว่าจะสร้าง mutable borrow ให้กับทุกสิ่งที่อยู่ลึกเข้าไปในฟิลด์นั้นได้เสมอไป ต้องมีกฎแยกต่างหาก
  • ตัวอย่างหลังจากนี้ใช้รูปแบบที่ชัดเจนกว่าอย่าง Rc Spaceship แทน syntax sugar shared mut type Spaceship
    • shared mut type Spaceship จะกลายเป็น type Spaceship และ var ship: Spaceship จะกลายเป็น var ship: Rc Spaceship

จุดที่ union สร้างปัญหาด้านความปลอดภัย

  • union เก็บเนื้อหาแบบ inline ได้ จึงลดการไล่ pointer และ cache miss ซึ่งเป็นผลดีต่อ ความเร็ว
    • เมื่อ union Engine ของ C อยู่ภายใน struct Spaceship ทั้ง StringTheoryEngine และ ImpulseEngine จะอยู่ในหน่วยความจำของ Spaceship
    • ตรงข้ามกับแนวทางแบบ Java ที่ใช้อินเทอร์เฟซและ pointer
  • ปัญหาคือการรองรับ union อย่างปลอดภัยในภาษาที่ memory-safe ทำได้ยาก
  • ในตัวอย่างที่ Engine เป็น StringTheoryEngine(str: String) หรือ ImpulseEngine(fuel: I32) หาก ship และ other_ship ชี้ไปยัง Spaceship เดียวกัน อาจเกิด segmentation fault ได้
    • หลังจากจับ reference ภายใน string ด้วย match uniq ship.engine
    • แล้วเปลี่ยน engine เดียวกันเป็น variant อื่นด้วย other_ship.engine := ImpulseEngine 0x42
    • จากนั้นแก้ไข str เดิม ก็จะเกิดปัญหาใช้งานสิ่งที่อยู่ข้างในหลังจาก container ถูกทำลายไปแล้ว
  • ดังนั้น Ante ต้องห้ามไม่ให้สร้าง mutable borrow reference ไปยัง variant ใด variant หนึ่ง เมื่อ mutable borrow reference ชี้ไปยัง union
  • กฎนี้ตรงข้ามกับกฎของ struct
    • หากมี mut reference ไปยัง struct สามารถสร้าง mut reference ไปยังฟิลด์ได้
    • หากมี mut reference ไปยัง union จะสร้าง mut reference ไปยังสิ่งที่อยู่ภายใน variant ไม่ได้

uniq และ temporary uniq conversion

  • uniq หมายถึง exclusive mutable reference หรือ reference แบบ mutable ที่เป็นเอกสิทธิ์
  • หากตัวแปรหนึ่งถือ uniq Spaceship อยู่ นั่นคือ reference เดียวที่ใช้งานได้ไปยัง Spaceship นั้น
    • เป็นแนวคิดคล้าย &mut Spaceship ของ Rust
  • เพื่อจัดการภายใน union อย่างปลอดภัย Ante ใช้ temporary uniq conversion
  • กฎหลักคือ หากไม่ใช้ reference อื่นที่อาจเป็น alias ในขอบเขตหนึ่ง ๆ ก็สามารถได้ uniq reference ชั่วคราว
    • ในช่วง match uniq ship.engine จะเข้าถึง ship.engine เสมือนเป็น uniq
    • ระหว่างช่วงนี้ compiler จะไม่อนุญาตให้ใช้ตัวแปรเดิมอื่นที่อาจบรรจุ Spaceship ทางอ้อมได้
  • Rust ป้องกันการมีอยู่ของ uniq เองด้วยเหตุผลว่า “อาจมี reference อื่นอยู่ที่ไหนสักแห่ง” แต่ Ante อนุญาต uniq ภายใต้เงื่อนไขว่า ไม่ใช้ reference เหล่านั้นในขอบเขตนั้น
  • ในกรณีนี้ uniq Spaceship ไม่ได้เป็น reference เดียวทั่วทั้งโปรแกรมจริง ๆ แต่เป็น reference เดียวที่ใช้งานได้ภายในขอบเขตนั้น
    • ให้ความรู้สึกคล้าย pointer แบบ restrict ใน C

การเข้าถึงที่อนุญาตและถูกปฏิเสธ

  • ภายในขอบเขต match uniq ship.engine หากเข้าถึง other_ship: Rc Spaceship ควรเกิด compile error
    • เพราะ other_ship.engine อาจเป็น alias กับ ship.engine
    • และระหว่างที่ใช้ ship.engine การเปลี่ยน other_ship.engine อาจทำให้เกิด drop ได้
  • struct อื่นที่มี Rc Spaceship เป็นฟิลด์ เช่น HasAShip ก็ถูกปฏิเสธด้วยเหตุผลเดียวกัน
    • other.ship.engine ก็อาจไปถึง Spaceship เดียวกันทางอ้อมได้
  • ในทางกลับกัน สามารถใช้จำนวนเต็มอย่าง new_fuel: I32 ได้
    • เพราะ I32 ไม่สามารถบรรจุ reference ไปยัง Spaceship ได้
  • หาก Spaceship เองมีฟิลด์อย่าง follow_ship: Rc Spaceship ก็จะถูกปฏิเสธ
    • ในกรณีนั้น uniq Spaceship ก็จะกลับไปถึงตัวเองได้ผ่านเส้นทางภายในตัวมันเอง ดังนั้นโดยทั่วไปจึงไม่สามารถแปลง mut -> uniq กับ recursive type ได้

ข้อจำกัดในการเรียกและคืนค่าฟังก์ชัน

  • mut -> uniq conversion อาจเกิดขึ้นในการเรียกฟังก์ชันด้วย
  • เมื่อ foo (var ship: Rc Spaceship) (new_res: Resonator) เรียก maybe_use_resonator ship new_res ที่จุดเรียก ship จะถูกแปลงเป็น uniq Spaceship
    • compiler เพียงต้องตรวจสอบว่าอาร์กิวเมนต์อื่นอาจมี reference ไปยัง Spaceship หรือไม่
    • Resonator ในตัวอย่างไม่มี reference แบบนั้น จึงอนุญาต
  • ในการคืนค่า ไม่สามารถคืน reference uniq ที่ถูกแปลงแล้วเป็น uniq ปกติได้
    • เพราะหลังจากคืนค่าแล้ว การตรวจของ compiler ที่ว่า “ไม่ใช้ตัวแปรที่อาจเป็น alias ภายในขอบเขต” จะไม่ถูกนำมาใช้
  • แต่สามารถกำหนด return type เป็น local uniq Foo ได้
    • ภายใน เมื่อแปลงจาก mut ref เป็น uniq ref สิ่งที่ถูกสร้างจริง ๆ จะเป็น local uniq เสมอ
    • ในกรณีส่วนใหญ่ใช้ได้เหมือน uniq ปกติ แต่เมื่อต้องคืนค่าจำเป็นต้องระบุให้ชัดเจน

ต้นทุนเชิงการออกแบบและทางเลือก

  • Ante สามารถเปลี่ยน reference counted reference อย่าง Rc Spaceship ให้เป็น uniq Spaceship ชั่วคราวได้โดยไม่มี runtime error
  • ข้อเสียคือ compiler ต้องไล่ดู type แบบ recursive เพื่อตอบคำถามอย่าง “จาก Engine สามารถไปถึง Spaceship ได้หรือไม่”
  • การวิเคราะห์แบบนี้อาจเปราะบาง
    • การเพิ่มฟิลด์ให้ struct อาจกลายเป็น breaking API change ได้
  • Jake ผู้สร้าง Ante กำลังมองหาวิธีที่ดีกว่าในการรักษาการรับประกันนี้
    • แนวทางที่ติดชนิด brand เฉพาะแบบไม่ระบุชื่อให้กับแต่ละ shared mutable type เช่น group borrowing และ Flix references
    • แนวทางที่เพิ่ม effect เช่น Mutates 'a เมื่อเปลี่ยน shared type เพื่อตัดการวิเคราะห์ type ออกไป
    • แนวทางที่ให้ผู้ใช้ตรวจตอนรันไทม์ว่า reference สองตัวชี้ไปคนละอ็อบเจกต์หรือไม่ หรือให้ unsafe check ที่ห่อด้วย safe API
    • แนวทางที่ compiler ติดตามค่าที่ไม่ได้ถูกเก็บทางอ้อมภายใน Rc จึงไม่อาจถูก alias ได้
  • แนวคิดที่คล้าย iso permission ของ Pony หรือสิทธิ์ชั่วคราวที่มองเข้าไปข้างใน struct ได้แต่ห้ามใช้ reference ที่ชี้ออกไปข้างนอก ก็ยังเป็นความเป็นไปได้
  • ส่วนที่ยากคือการรักษา ความใช้งานง่าย, ความอ่านง่าย และ ความเรียบง่าย ซึ่งเป็นเป้าหมายของ Ante ไว้ ขณะยังคงความยืดหยุ่นเช่นนี้

กระแสที่กว้างขึ้นของความปลอดภัยหน่วยความจำ

  • shared mutable borrowing เคยถูกมองว่าเป็นไปไม่ได้ และมีมุมมองว่า Rust ก็ถูกออกแบบบนความเชื่อนั้น
  • ข้อยกเว้นต่าง ๆ กำลังสะสมมากขึ้น
    • Ante สามารถได้ uniq borrow reference จากข้อมูล shared-mutable ผ่านกฎ local uniqueness
    • Vale สามารถได้ immutable borrow reference จากข้อมูล shared-mutable ผ่าน pure function
    • group borrowing สามารถสร้าง shared-mutable borrow reference ได้แม้ไม่ใช่ shape-stable
    • GhostCell ของ Rust อนุญาตให้กราฟของอ็อบเจกต์ชี้หากันได้อย่างอิสระ แต่ ณ เวลาใดเวลาหนึ่งจะมี mutable reference ได้เพียงหนึ่งตัวไปยังหนึ่งในนั้น
  • กระแสนี้บ่งชี้ว่าอาจมีหลักการที่ทั่วไปกว่าสำหรับจัดการ shared mutable borrowing ในการออกแบบความปลอดภัยหน่วยความจำ

เปรียบเทียบกับ Cell ของ Rust

  • ผู้ใช้ Rust อาจถามว่าการใส่ Cell ในฟิลด์ของ struct ต่างจากแนวทางของ Ante อย่างไร
  • ในตัวอย่าง Ante สามารถได้ reference mut String ไปยัง status: String จาก Rc Spaceship แล้วต่อ " (refueling)" เข้าไปโดยตรง
  • ในแนวทาง Cell<String> ของ Rust ไม่สามารถได้ &mut String จาก Rc<Spaceship>
    • แต่ต้องใส่ค่าพื้นฐานชั่วคราวด้วย status_ref.replace(String::new())
    • แก้ไข String ที่ดึงออกมา
    • แล้วสุดท้ายใส่กลับด้วย replace(status)
  • วิธีนี้มีข้อเสียหลายอย่าง
    • ต้องสร้าง อินสแตนซ์พื้นฐาน เช่น ""
    • มีความเสี่ยงที่จะลืมเรียก replace ครั้งสุดท้าย
    • มีความเสี่ยงที่บางคนจะอ่าน status ขณะที่ค่าถูกแทนที่อยู่
  • Ante อนุญาตให้ได้ reference ไปยัง string status ชั่วคราว และ compiler จะบังคับไม่ให้โค้ดอื่นเข้าถึงในระหว่างนั้น

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 4 시간 전
ความคิดเห็นจาก Lobste.rs

  • ที่เคยคิดว่า “shared mutable borrow” เป็นไปไม่ได้นั้น ไม่ใช่แค่ข้อแลกเปลี่ยนที่ Rust ยอมรับเพื่อให้บรรลุเป้าหมาย แต่แทบจะเป็นเป้าหมายแกนหลักของ Rust เอง
    เพราะสถานะที่แก้ไขได้และถูกแชร์ร่วมกันทำให้การ ให้เหตุผลเฉพาะที่ กับโค้ดยากขึ้น
    "References are like jumps" by withoutboats อธิบายประเด็นนี้ได้ดีมาก ประเด็นสำคัญคือการป้องกันไม่ให้สถานะที่มี alias ถูกแก้ไขโดยไม่ตั้งใจ เพื่อให้สร้างระบบที่ทำงานได้ถูกต้องได้ง่ายขึ้น และกฎ lifetime ของ Rust ก็ไม่ใช่แค่อุปกรณ์สำหรับหลีกเลี่ยง garbage collection แต่เป็นโครงสร้างที่ลึกกว่านั้นเพื่อรักษาความสามารถในการให้เหตุผลในภาษาที่อนุญาตทั้งสถานะแบบ mutable และสถานะแบบ alias พร้อมกัน

    • ตอนที่ผู้เขียนเคยพูดถึง Mojo borrow checker ก็รู้สึกแบบเดียวกัน Rust borrow checker ช่วยรักษา value semantics ไว้ได้ แม้ในโปรแกรมแบบเธรดเดียว

  • ดูค่อนข้างดีทีเดียว
    ถ้าเข้าใจไม่ผิด เวทมนตร์ที่เปลี่ยนจาก shared reference ไปเป็น mutable reference ทำได้เพราะจำกัดอยู่กับชนิดที่ไม่ถูกแชร์ข้ามเธรด และความเป็นเอกลักษณ์ของ Rc ก็ดูเหมือนจะรับประกันโดยมองว่าวัตถุทั้งหมดของชนิดเดียวกันถูกยืมด้วย lifetime เดียวกัน
    เรื่องไวยากรณ์แบบชัดเจนหรือแบบเป็นธรรมชาติดีกว่ากันอาจเป็นเรื่องรสนิยม แต่ก็แสดงให้เห็นว่าถ้าคอมไพเลอร์รู้จัก Cell มากขึ้น ก็อาจอนุญาต mutable reference ไปยังมันได้ยืดหยุ่นกว่าเดิม
    และยังเลี่ยงการใช้คำที่ทำให้สับสนแบบใน Rust ที่ mut ถูกใช้ในความหมายว่า exclusive/unique มากกว่าจะหมายถึง mutable

    • ผมก็สงสัยเหมือนกันว่าแล้วข้ามเธรดจะเป็นอย่างไร คำถามประมาณว่า “การยกระดับ uniq หมายถึงการ acquire lock หรือเปล่า?” แต่ดูเหมือนต้องเข้าใจว่าเขาเทียบกับ Rc ไม่ใช่ Arc
    • ช่วยอธิบายเพิ่มได้ไหมว่าที่บอกว่า mut หมายถึง exclusive/unique คืออะไร?

  • อยากรู้ว่ามีใครพอเดาได้ไหมว่า หลักการรวมศูนย์ ที่ผู้เขียนใบ้ไว้ตอนท้ายนั้นคืออะไร

  • การอภิปรายก่อนหน้านี้เกี่ยวกับโพสต์ในบล็อก antelang.org ก็น่าดูเหมือนกัน

  • ผมยังไม่ค่อยเข้าใจว่ามันทำงานอย่างไร ดูเหมือนว่ามันจะบอกว่า “ถ้ามี mutable pointer ไปยังออบเจ็กต์หนึ่ง ก็สามารถเอา modifying reference ไปยัง slice ของออบเจ็กต์นั้นได้”
    แต่ถ้าอย่างนั้นก็ดูเหมือนจะเขียนอะไรแบบ mutref someobjext = …, mutref subfield = someobjext.a.b, someobjext.a = somethingelse ได้ และถ้าเป็นแบบนั้น subfield ก็อาจใช้ไม่ได้อีกต่อไป หรือพังเพราะค่าถูกเปลี่ยนไป
    ในบทความมีทั้งคำอธิบาย การเปรียบเทียบกับภาษาอื่น และตัวอย่างโค้ดมากมาย แต่กลับหาส่วนที่สรุป ความหมายเชิงลำดับขั้น ของการทำงานนี้แบบพื้นฐานจริง ๆ ได้ยาก