Tree Borrows

 (plf.inf.ethz.ch)
1 คะแนน โดย GN⁺ 2025-07-10 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • เสนอ Tree Borrows ซึ่งเป็นโมเดลหน่วยความจำแบบใหม่เพื่อก้าวข้ามข้อจำกัดด้านการเพิ่มประสิทธิภาพของโค้ด unsafe ในภาษา Rust
  • Tree Borrows แก้ปัญหาที่แนวทาง Stacked Borrows เดิมไม่สามารถยอมรับหลายแพตเทิร์นที่ใช้บ่อยในโค้ด Rust จริงได้ โดยใช้โครงสร้างแบบต้นไม้ ทำให้ได้กฎที่สมจริงและยืดหยุ่นยิ่งขึ้น
  • Tree Borrows ผ่านกรณีทดสอบโค้ดจริงได้มากกว่า Stacked Borrows 54%
  • ยังคงรักษาคุณสมบัติสำคัญด้านความปลอดภัยของหน่วยความจำและความสามารถในการเพิ่มประสิทธิภาพของ Rust ไว้เป็นส่วนใหญ่ (โดยเฉพาะ read-read reordering เป็นต้น) พร้อมทั้งสะท้อนฟีเจอร์ขั้นสูงของ borrow checker รุ่นใหม่ของ Rust ได้ด้วย
  • นำเสนอ โมเดล state machine แบบอิงโครงสร้างต้นไม้ ซึ่งเป็นหมุดหมายสำคัญสำหรับงานวิจัยด้านการเพิ่มประสิทธิภาพและการตรวจสอบความปลอดภัยของ Rust

ระบบ ownership ของ Rust และข้อจำกัดของโค้ด unsafe

  • Rust มอบการรับประกันที่แข็งแกร่ง เช่น ความปลอดภัยของหน่วยความจำและการป้องกัน data race ผ่าน ระบบชนิดข้อมูลที่อิง ownership
  • อย่างไรก็ตาม Rust มี unsafe escape hatch อยู่ ซึ่งในกรณีนี้ความรับผิดชอบในการตรวจสอบความปลอดภัยจะย้ายจากคอมไพเลอร์ไปยังนักพัฒนา
  • คอมไพเลอร์ต้องการใช้กฎการ alias ของพอยน์เตอร์เพื่อทำการเพิ่มประสิทธิภาพอย่างเข้มข้น แต่โค้ด unsafe ที่ไม่ถูกต้องอาจทำให้การเพิ่มประสิทธิภาพเหล่านี้ใช้ไม่ได้ผล

Stacked Borrows และข้อจำกัดของมัน

  • เดิมมีโมเดลชื่อ Stacked Borrows ที่ใช้กำหนดว่าอะไรคือ “พฤติกรรมที่ไม่ถูกต้อง” ของโค้ด unsafe และใช้เป็นเกณฑ์สำหรับการเพิ่มประสิทธิภาพ
  • แต่แนวทางนี้ ไม่สามารถยอมรับแพตเทิร์น unsafe หลายแบบที่พบได้บ่อยในโค้ด Rust จริง และยังไม่สะท้อนฟีเจอร์ของ borrow checker ของ Rust ที่เพิ่งถูกนำเข้ามาในช่วงหลัง

การมาของ Tree Borrows

  • Tree Borrows คือโมเดลใหม่ที่ติดตามสิทธิ์ในการเข้าถึงหน่วยความจำด้วย โครงสร้างแบบต้นไม้แทนโครงสร้างแบบซ้อนทับ (stack)
  • ด้วยเหตุนี้จึง ยอมรับแพตเทิร์นโค้ด Rust ที่ใช้จริงได้อย่างปลอดภัยมากขึ้น และเพิ่มทั้งความยืดหยุ่นของกฎการ borrow และความเหมาะสมต่อการใช้งานจริงอย่างมาก
  • จากการประเมิน popular crate ของ Rust จำนวน 30,000 รายการ พบว่า ผ่านกรณีทดสอบได้มากกว่า Stacked Borrows 54%

คุณลักษณะและข้อดีของ Tree Borrows

  • ยังคงรักษา การเพิ่มประสิทธิภาพสำคัญ ของ Stacked Borrows เดิมไว้ได้เป็นส่วนใหญ่ (เช่น read-read reorderings)
  • นอกจากนี้ยังรองรับฟีเจอร์ขั้นสูงของ borrow checker รุ่นใหม่ของ Rust ได้ด้วย (เช่น แพตเทิร์นการ borrow ที่ไม่เป็นรูปแบบตายตัว การจัดการพอยน์เตอร์ที่ซับซ้อน เป็นต้น)
  • นำเสนอ โมเดล state machine แบบอิงต้นไม้ เพื่อสร้างสมดุลระหว่างความปลอดภัยและความสามารถในการเพิ่มประสิทธิภาพ

บทสรุปและความสำคัญ

  • Tree Borrows นำเสนอ มาตรฐานใหม่ สำหรับการจัดการโค้ด unsafe และงานวิจัยด้านการเพิ่มประสิทธิภาพของคอมไพเลอร์ Rust
  • ได้รับการประเมินว่าเป็น โมเดลหน่วยความจำที่สมจริงและแข็งแกร่ง ซึ่งครอบคลุมทั้งโค้ด Rust ที่ใช้จริงและนโยบายล่าสุดของ borrow checker
  • งานวิจัยฉบับเต็ม อาร์ติแฟกต์ และซอร์สโค้ดที่เกี่ยวข้องได้ถูกเผยแพร่แล้ว และคาดว่าจะส่งผลอย่างมากต่อชุมชนวิจัยด้านคอมไพเลอร์และการตรวจสอบความถูกต้องของ Rust

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

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

 
GN⁺ 2025-07-10
ความคิดเห็นบน Hacker News

  • โพสต์บล็อกล่าสุดของ Ralf Jung ให้บริบทเพิ่มเติมไว้ ลิงก์
    โบนัส: ขอแนะนำวิดีโอล่าสุดของกลุ่มวิจัยที่พยายามระบุ operational semantics ของ Rust ให้ชัดเจนด้วยภาษาถิ่นของ Rust เอง YouTube

  • มีการอ้างว่าจากมุมมองของคอมไพเลอร์ การใช้ประโยชน์จากการรับประกันที่เข้มแข็งของ type system เกี่ยวกับ pointer aliasing ทำให้ทำ optimization ที่ทรงพลังได้ แต่ก็สงสัยว่าในทางปฏิบัติแล้วได้ผลแค่ไหน
    Linus Torvalds พูดมานานแล้วว่ากฎ strict aliasing ของ C แทบไม่มีประโยชน์และกลับสร้างปัญหามากกว่า
    โพสต์ ตัวอย่าง ของเขาก็น่าสนใจ
    เลยสงสัยว่า Rust ต่างจาก C โดยพื้นฐานจริงหรือไม่ เพราะจากประสบการณ์ส่วนตัว โดยเฉพาะเมื่อมี unsafe เข้ามาเกี่ยว ก็รู้สึกว่าแทบไม่ต่างกัน

    • คิดว่ากฎ strict aliasing ของ C แย่มากจริง ๆ
      กฎที่ Rust เสนอนั้นต่างออกไปมาก และมองว่ามีประโยชน์กับคอมไพเลอร์มากกว่า รวมถึงสร้างภาระให้โปรแกรมเมอร์น้อยกว่า
      มี in-language opt-out โดยใช้ raw pointer ได้ และยังมีเครื่องมือช่วยตรวจโค้ดได้ด้วย
      ท้ายที่สุดก็เป็นการประนีประนอมเหมือนการออกแบบภาษาทุกแบบ
      ดูเหมือนว่า Rust จะหาสมดุลใหม่ในพื้นที่ optimization นี้ได้แล้ว และผลของการตัดสินใจนั้นคงต้องให้เวลาเป็นตัวพิสูจน์

    • กฎ aliasing ของ Rust ต่างจาก C มาก
      ใน C นั้นคีย์เวิร์ด restrict แทบจะมีความหมายเฉพาะกับ argument ของฟังก์ชัน และ type-based aliasing ก็แทบไม่ค่อยถูกใช้จริงหรือใช้งานลำบาก
      ใน Rust สามารถแสดง lifetime และ mutability ได้อย่างละเอียด และจัดการหน่วยความจำอย่างปลอดภัยได้หลายรูปแบบโดยไม่ขึ้นกับ type เอง
      จุดสำคัญคือห้ามมี &mut ที่ซ้อนทับกัน แต่ยังแบ่งเป็น &mut หลายตัวที่ไม่ทับซ้อนกันเพื่อใช้งานได้

    • อยากเห็นการวิเคราะห์ที่กว้างกว่านี้ว่าในความเป็นจริงมันส่งผลต่อประสิทธิภาพมากแค่ไหน
      ถ้าลบส่วนที่ส่งข้อมูล aliasing ไปยัง LLVM ออกจากคอมไพเลอร์ทั้งหมด แล้วเปรียบเทียบประสิทธิภาพ ก็น่าจะเห็นได้ทันที
      มีคอมเมนต์ นี้ ที่อ้างว่า annotation noalias ช่วยเพิ่มประสิทธิภาพรันไทม์ได้ราว 5% (แม้ว่าข้อมูลจะค่อนข้างเก่าแล้ว)

    • เวลาฟัง Linus พูดเรื่องคอมไพเลอร์ก็ควรเผื่อใจไว้บ้าง
      เคอร์เนลระบบปฏิบัติการกับคอมไพเลอร์เป็นคนละโลกกันเลย
      ทุกวันนี้ alias analysis เป็นหัวใจสำคัญของการเพิ่มประสิทธิภาพอย่างมาก
      ผลลัพธ์ที่ใหญ่ที่สุดมาจาก heuristic แบบง่าย ๆ ส่วน alias query ที่ซับซ้อนนั้นตัวมันเองกลับมีประโยชน์จำกัด
      ในทางทฤษฎีอยากลองทดลองดูว่า alias analysis ที่สมบูรณ์แบบจะเพิ่มประสิทธิภาพได้มากแค่ไหน แต่กับโค้ดทั่วไปก็น่าจะมีเพดานราว 20%
      แน่นอนว่า optimization ขั้นสูงมากบางอย่าง เช่น การแปลง data layout จะเป็นสิ่งที่ไม่กล้าลองทำเลยหากไม่มี alias analysis

    • strict aliasing ของ C กับ aliasing ของ Rust เป็นคนละแนวคิดกัน
      ของ C มี TBAA เป็นแกนหลัก และ Rust ก็จงใจไม่รับแนวทางนั้นมาใช้

  • เคยมีเธรดเก่าเกี่ยวกับ Stacked Borrows ในปี 2020 และ 2018
    เธรดปี 2020
    เธรดปี 2018

  • เคยอ่านสเปก Tree Borrows บนเว็บไซต์ของ Nevin เมื่อหลายปีก่อน และประทับใจที่มันแก้ปัญหาซับซ้อนได้อย่างสง่างาม
    จาก ประสบการณ์จริง Tree Borrows ทำให้เขียนโค้ดที่สมเหตุสมผลซึ่งเป็นไปไม่ได้ภายใต้ Stacked Borrows ได้
    โค้ด ตัวอย่าง ในไลบรารีมาตรฐานของ Rust ก็น่าดูเช่นกัน

  • สงสัยว่า Rust หรือ PL รุ่นถัดไปจะพัฒนาไปถึงจุดที่สามารถเลือกใช้ borrow checker หลายแบบ ซึ่งมีคุณสมบัติและเป้าหมายต่างกัน เช่น ความเร็วคอมไพล์ ความเร็วรันไทม์ ความยืดหยุ่นของอัลกอริทึม ได้หรือไม่

    • Rust รองรับการเปลี่ยน implementation ของ borrow checker อยู่แล้ว
      มันเปลี่ยนจากแบบอิง scope ไปเป็น non-lexical และยังมี implementation เชิงทดลองชื่อ Polonius ให้เลือกด้วย
      เมื่อ implementation ใหม่พร้อมใช้งาน ก็ไม่ได้มีเหตุผลต้องเก็บของเก่าไว้
      และยังเลือกใช้แบบยืดหยุ่นกว่านี้ได้ผ่านการตรวจสอบตอนรันไทม์อย่าง Rc, RefCell เป็นต้น

    • มีแนวทางอยู่แล้วหลายแบบ เช่น affine type (ที่ Rust ใช้), linear type, effect system, dependent type, formal proof
      แต่ละแบบก็มีลักษณะแตกต่างกันทั้งด้านต้นทุนการใช้งาน ประสิทธิภาพ และประสบการณ์การพัฒนา
      แม้นอกเหนือจาก Rust ก็มีแนวโน้มที่จะมุ่งหาการผสมกันระหว่างการจัดการทรัพยากรอัตโนมัติที่มีประสิทธิภาพกับ type system

    • สิ่งที่ต้องการจริง ๆ คือ separation logic ที่สามารถระบุ precondition ของฟังก์ชันได้อย่างแม่นยำ และพิสูจน์เงื่อนไขระหว่างทางได้ด้วย
      แนวทางของ Rust คือการทำให้ invariants แบบทั่วไปที่ผู้คนต้องการจริง ๆ กลายเป็นระบบ เพื่อรับประกัน optimization ที่ทรงพลัง

    • สงสัยว่าผลของ borrow checker จะมีแต่ false negative และไม่มี false positive จริงไหม
      ถ้าเป็นเช่นนั้น ก็อดคิดไม่ได้ว่าจะเอา implementation หลายตัวมารันขนานกันในหลายเธรด แล้วใช้ผลจากตัวที่เสร็จก่อนสุดได้หรือไม่

    • ถ้ายอมให้มี implementation ของ borrow checker หลายแบบพร้อมกัน ก็มีโอกาสสูงที่ ecosystem จะแตกเป็นเสี่ยง ๆ จึงไม่ค่อยเป็นแนวทางที่พึงประสงค์

  • ลองทดสอบโค้ด Rust ในบทความจริงแล้ว และยืนยันได้ว่าคอมไพเลอร์เวอร์ชันเสถียรล่าสุดไม่ได้ปฏิเสธมัน
    ตัวอย่างโค้ด:

    fn write(x: &mut i32) {*x = 10}

fn main() {
  let x = &mut 0;
  let y = x as *mut i32;
  //write(x); 
  *x = 10; 
  unsafe {*y = 15 };
}
    • Stacked Borrows เป็นโมเดลรันไทม์ของ miri
      ถ้าลองรันโค้ดข้างต้นใน miri มันจะรายงานข้อผิดพลาดที่ *x = 10; แต่จะไม่เกิดข้อผิดพลาดใน write(x);
      rustc มองจากมุมของ type system ว่า y เป็น *mut ดังนั้นจึงไม่มีเหตุผลที่จะปฏิเสธทั้งสองแบบ

  • ในบทความยกตัวอย่างโค้ดด้านล่างว่าเป็นปัญหาของ unsafe code:

    fn main() {
  let mut x = 42;
  let ptr = &mut x as *mut i32;
  let val = unsafe { write_both(&mut *ptr, &mut *ptr) };
  println!("{val}");
}

    เลยสงสัยว่าสิ่งนี้เกิดขึ้นได้จริงหรือ
    การใช้ pointer เพื่อสร้าง mutable reference หลายตัวให้กับตัวแปรเดียวกันนั้นชัดเจนว่าเป็น UB อยู่แล้ว เลยสงสัยว่าตัวเองเข้าใจอะไรผิดไปหรือไม่

    • แก่นของงานวิจัยนี้คือการกำหนดขอบเขตของ UB (undefined behavior) ให้ชัดเจนและแม่นยำ
      โค้ดข้างต้นถึงคอมไพเลอร์ Rust จะยอมรับ แต่ก็ยังละเมิดกฎ
      กฎอะไร?

  • โค้ดที่ผ่าน borrow checker ถือว่าถูกต้อง

  • unsafe สามารถแสดงสิ่งที่ผิดกฎหมายหรือเป็น UB ได้

  • มีกลุ่มกฎที่กว้างกว่าเขตของ borrow checker แต่ยังถือว่าถูกต้องอยู่
    งานวิจัยนี้มีจุดประสงค์เพื่อระบุขอบเขตนั้นอย่างเข้มงวด
    บทความ Stacked Borrows เรียบง่ายกว่า แต่มีข้อจำกัดกับ unsafe code ในโลกจริง ส่วน Tree Borrows ยอมรับขอบเขตที่ปลอดภัยได้กว้างกว่า

    • แน่นอนว่า "ไม่สามารถมี mutable reference หลายตัวพร้อมกันได้" แต่ก็ไม่มีจุดไหนที่ระบุชัดเจนว่ามันละเมิดกฎข้อใดกันแน่
      Tree Borrows เสนอคำจำกัดความแบบนั้นพอดี
      การพูดว่า "โค้ดทำสิ่งนี้ได้" หมายถึง ถ้าคุณเขียนและรันโค้ดนั้นจริง มันจะมีบางอย่างเกิดขึ้น แต่หากไม่มีนิยามชัดเจนแบบ Tree Borrows ก็ยากจะมีหลักฐานว่าทำไมสิ่งนี้จึงผิด
      ดูเหมือนว่าคุณเองก็ยอมรับความจำเป็นของกฎที่ชัดเจนแบบ Tree Borrows อยู่แล้ว

    • unsafe code แบบนั้นเกิดขึ้นได้จริง และนั่นแหละคือความเป็น UB
      ตัวอย่าง: ลิงก์ playground

    • ถ้าอยากเข้าใจบริบทที่เกี่ยวข้อง ช่วงต้นของย่อหน้าถัดไปในบทความอธิบายเจตนาไว้ชัดมาก

หากนักพัฒนาคอมไพเลอร์ Rust ต้องการ optimization ด้าน aliasing พวกเขาจำเป็นต้องมีวิธีตัดโค้ดโต้แย้งอย่างตัวอย่างข้างต้นออกไป

  • ใช่ นี่แหละประเด็น
    การรักษากฎห้ามมี mutable reference หลายตัวนั้นทำได้ยาก และสะท้อนว่า unsafe อนุญาตได้มากกว่าสิ่งที่ระบบ lifetime ของ Rust รับประกันไว้อย่างมาก

  • Neven Villani หนึ่งในผู้เขียน เป็นลูกชายของ Cédric Villani ผู้ได้รับ Fields Medal ปี 2010
    ทำให้นึกถึงคำเปรียบเปรยว่าลูกไม้ย่อมหล่นไม่ไกลต้น

    • และก็อยากเล่นคำขำ ๆ ว่า “คุณสมบัติต่าง ๆ ก็คง borrow มาจาก tree เหมือนกัน”

    • ผมเองก็เคยมีสำนักงานอยู่ใกล้กับพ่อของเขา (ผู้ได้ Fields Medal) ด้วย
      เป็นช่วงก่อนที่เขาจะเข้าสู่การเมือง

  • โมเดลนี้ยอดเยี่ยมจริง ๆ
    มีแผนจะลองนำไปใช้ในภาษาที่กำลังทำอยู่ด้วย

  • ไม่น่าใช่เดจาวู
    รู้สึกเหมือนเห็นโพสต์นี้โผล่มาทุก ๆ 2-3 เดือน

    • เพราะบทความนี้เตรียมกันมาหลายปี และในที่สุดก็ได้รับการตีพิมพ์อย่างเป็นทางการ