Ante: Cách tiếp cận mới kết hợp kiểm tra mượn và đếm tham chiếu

 (verdagon.dev)
1 điểm bởi GN⁺ 4 giờ trước | 1 bình luận | Chia sẻ qua WhatsApp
  • Ante là một thiết kế ngôn ngữ hệ thống nhằm kết hợp tính linh hoạt của đếm tham chiếu với độ an toàn của kiểm tra mượn, đồng thời tránh panic lúc chạy kiểu Rust hay chi phí kiểm tra truy cập độc quyền kiểu Swift
  • Cơ chế cốt lõi là shape-stability và temporary uniq conversion, cho phép tạo mượn khả biến một cách an toàn cho các trường của giá trị được đếm tham chiếu, đồng thời chỉ xử lý giá trị bên trong union như uniq trong phạm vi hạn chế
  • Rc<RefCell<T>> của Rust nếu dùng sai có thể gây panic lúc chạy, còn hệ thống borrowing của Swift bao gồm kiểm tra truy cập độc quyền lúc chạy; Ante cố gắng xử lý một số trường hợp bằng quy tắc ở thời điểm biên dịch
  • Đây vẫn là một thiết kế work-in-progress mới chỉ được triển khai một phần; vì cần phân tích kiểu một cách đệ quy để xác định có thể đi tới một đối tượng cụ thể hay không, việc thêm trường có thể trở thành breaking API change
  • Cách tiếp cận này làm suy yếu giả định rằng shared mutable borrowing luôn là bất khả thi, qua đó mở rộng vùng ngoại lệ trong thiết kế an toàn bộ nhớ cùng với các kỹ thuật như Vale, group borrowing và Rust GhostCell

Sự kết hợp mà Ante hướng tới

  • Ante là một ngôn ngữ lập trình hệ thống hướng tới một phiên bản Rust đơn giản hơn nhưng vẫn có an toàn bộ nhớ và an toàn luồng
  • Mô hình cơ bản là quyền sở hữu đơn và kiểm tra mượn, trong đó giá trị được đặt nội tuyến trên stack hoặc bên trong struct/mảng bao chứa nó
  • Khi muốn ưu tiên sự đơn giản, có thể thêm từ khóa shared vào kiểu để chọn dùng đếm tham chiếu
  • Với shared type Color, shared type RbTree t, hàm balance của red-black tree ngắn gần như ví dụ Python và ngắn hơn ví dụ C++ hay Rust
  • Mối quan tâm chính là cách mượn dữ liệu được đếm tham chiếu theo kiểu khả biến mà không gặp nguy cơ panic từ borrow_mut() của Rust hay kiểm tra truy cập độc quyền lúc chạy của Swift
  • Ante hiện vẫn ở trạng thái work-in-progress; một phần đã được triển khai, một phần vẫn mới ở mức lý thuyết, và thiết kế cũng đang tiếp tục thay đổi

shape-stability và nhiều tham chiếu khả biến

  • shape-stability của Ante là khái niệm rằng “tham chiếu tới một đối tượng có stable shape sẽ luôn hợp lệ dù các thay đổi khác xảy ra ở nơi khác”
  • Nhờ khái niệm này, có thể đồng thời có nhiều tham chiếu mượn khả biến tới cùng một struct
  • Trong ví dụ heal (healer: mut Entity) (target: mut Entity), có thể gọi self_heal bằng cách truyền cùng một Entity vào cả hai tham số để tự hồi máu
    • Dù healer và target cùng trỏ tới một Entity, đoạn mã này không thể phá hủy Entity, nên cả hai tham chiếu vẫn luôn hợp lệ
  • Cũng có thể đồng thời cho phép tham chiếu khả biến tới bản thân struct, tới trường của nó, và tới trường con của trường đó
    • Có thể dùng đồng thời ship: mut Spaceship và engine_alias: mut Engine = ship.engine, vì hệ thống xác định rằng trong lúc hàm chạy, ship và engine bên trong nó sẽ không bị phá hủy
  • Rust và Swift không cho phép nhiều tham chiếu &mut cùng lúc trỏ vào cùng một dữ liệu như vậy

Mượn khả biến các trường của giá trị được đếm tham chiếu

  • Trong Ante, nếu thêm shared trước định nghĩa kiểu thì kiểu đó sẽ tự động được đếm tham chiếu
  • Trong ví dụ shared mut type Spaceship, launch giữ một Spaceship tương đương Rc và truyền mut ship.engine vào set_fuel
  • Vì launch đang giữ đối tượng bao chứa là Spaceship, nên có thể kết luận rằng trường engine của nó cũng vẫn còn sống
  • Quy tắc chung là luôn có thể tạo tham chiếu mượn mut tới các trường của kiểu shared mut
    • Tuy nhiên, điều đó không có nghĩa là luôn có thể tạo mượn khả biến tới mọi đối tượng nằm sâu bên trong trường đó; phần này cần quy tắc riêng
  • Các ví dụ sau đó dùng ký hiệu tường minh hơn là Rc Spaceship thay cho cú pháp rút gọn shared mut type Spaceship
    • shared mut type Spaceship sẽ trở thành type Spaceship, còn var ship: Spaceship sẽ trở thành var ship: Rc Spaceship

Điểm mà union tạo ra vấn đề an toàn

  • Union lưu nội dung nội tuyến nên có lợi về tốc độ, vì giảm việc lần theo con trỏ và giảm cache miss
    • Nếu union Engine của C nằm trong struct Spaceship, thì StringTheoryEngine và ImpulseEngine sẽ nằm ngay trong bộ nhớ của Spaceship
    • Điều này đối lập với cách dùng interface và con trỏ như trong Java
  • Vấn đề là trong ngôn ngữ an toàn bộ nhớ, rất khó hỗ trợ union một cách an toàn
  • Trong ví dụ Engine là StringTheoryEngine(str: String) hoặc ImpulseEngine(fuel: I32), có thể xảy ra segfault khi ship và other_ship cùng trỏ tới một Spaceship
    • Sau khi giữ tham chiếu nội bộ của chuỗi bằng match uniq ship.engine
    • rồi đổi cùng engine đó sang biến thể khác bằng other_ship.engine := ImpulseEngine 0x42
    • sau đó tiếp tục sửa str cũ, ta sẽ rơi vào tình huống dùng dữ liệu bên trong sau khi container của nó đã bị phá hủy
  • Vì vậy, Ante phải ngăn việc tạo tham chiếu mượn khả biến tới một biến thể bên trong khi tham chiếu mượn khả biến đang trỏ tới union
  • Điều này trái ngược với quy tắc cho struct
    • Nếu có tham chiếu mut tới một struct, có thể tạo tham chiếu mut tới trường của nó
    • Nếu có tham chiếu mut tới một union, không thể tạo tham chiếu mut tới phần bên trong biến thể của nó

uniq và temporary uniq conversion

  • uniq nghĩa là exclusive mutable reference, tức tham chiếu khả biến độc quyền
  • Nếu một biến chứa uniq Spaceship, thì đó là tham chiếu duy nhất có thể dùng tới Spaceship đó
    • Khái niệm này tương tự &mut Spaceship của Rust
  • Để xử lý an toàn phần bên trong union, Ante dùng temporary uniq conversion
  • Quy tắc cốt lõi là nếu trong một phạm vi nhất định không dùng các tham chiếu khác có thể là alias, thì có thể tạm thời lấy được tham chiếu uniq
    • Trong vùng match uniq ship.engine, việc truy cập ship.engine được đối xử như uniq
    • Trong thời gian đó, trình biên dịch sẽ không cho phép dùng các biến hiện có khác có thể gián tiếp chứa Spaceship
  • Rust ngăn sự tồn tại của uniq chỉ vì “có thể có tham chiếu khác ở đâu đó”, còn Ante cho phép uniq với điều kiện các tham chiếu đó không được sử dụng trong phạm vi tương ứng
  • Khi đó uniq Spaceship thực tế không phải tham chiếu duy nhất trên toàn cục, mà là tham chiếu duy nhất có thể sử dụng trong phạm vi đó
    • Nó mang sắc thái gần giống con trỏ restrict của C

Các cách truy cập được chấp nhận và bị từ chối

  • Nếu truy cập other_ship: Rc Spaceship bên trong phạm vi match uniq ship.engine, thì phải báo lỗi biên dịch
    • Vì other_ship.engine có thể là alias của ship.engine
    • Và việc sửa other_ship.engine trong lúc đang dùng ship.engine có thể gây drop
  • Một struct khác như HasAShip chứa trường Rc Spaceship cũng bị từ chối vì cùng lý do
    • other.ship.engine cũng có thể gián tiếp đi tới cùng Spaceship
  • Ngược lại, có thể dùng số nguyên như new_fuel: I32
    • Vì I32 không thể chứa tham chiếu tới Spaceship
  • Nếu chính Spaceship có trường như follow_ship: Rc Spaceship thì cũng bị từ chối
    • Khi đó uniq Spaceship có thể lại đi tới chính nó qua đường dẫn nội bộ, nên nói chung không thể chuyển mut -> uniq với kiểu đệ quy

Ràng buộc ở lời gọi hàm và giá trị trả về

  • Chuyển đổi mut -> uniq cũng có thể xảy ra khi gọi hàm
  • Khi foo (var ship: Rc Spaceship) (new_res: Resonator) gọi maybe_use_resonator ship new_res, tại điểm gọi ship được chuyển thành uniq Spaceship
    • Trình biên dịch chỉ cần kiểm tra xem các đối số khác có thể chứa tham chiếu tới Spaceship hay không
    • Kiểu Resonator trong ví dụ không chứa tham chiếu như vậy nên được chấp nhận
  • Khi trả về, không thể trả tham chiếu uniq đã được chuyển đổi đó như một uniq thông thường
    • Sau khi trả về, kiểm tra của trình biên dịch rằng “không dùng các biến có thể alias trong phạm vi này” sẽ không còn áp dụng nữa
  • Thay vào đó, có thể khai báo kiểu trả về là local uniq Foo
    • Nội bộ, khi chuyển mut ref sang uniq ref, thứ thực sự được tạo ra luôn là local uniq
    • Trong đa số trường hợp nó dùng như uniq thông thường, nhưng khi trả về thì phải ghi rõ

Chi phí thiết kế và các phương án thay thế

  • Ante có thể biến tham chiếu đếm tham chiếu như Rc Spaceship thành uniq Spaceship tạm thời mà không gây lỗi lúc chạy
  • Điểm bất lợi là trình biên dịch phải đệ quy qua các kiểu để trả lời các câu hỏi như “từ Engine có thể đi tới Spaceship hay không”
  • Kiểu phân tích này có thể mong manh
    • Việc thêm trường vào struct có thể trở thành breaking API change
  • Jake, tác giả của Ante, đang tìm kiếm cách tốt hơn để giữ được bảo đảm này
    • Gắn một kiểu brand ẩn danh, duy nhất cho từng kiểu khả biến dùng chung, tương tự group borrowing và Flix references
    • Loại bỏ phân tích kiểu bằng cách thêm effect như Mutates 'a khi sửa kiểu dùng chung
    • Để người dùng tự kiểm tra lúc chạy xem hai tham chiếu có trỏ tới hai đối tượng khác nhau hay không, hoặc cung cấp kiểm tra unsafe được bọc trong API an toàn
    • Để trình biên dịch theo dõi các giá trị không được lưu gián tiếp trong Rc nên không thể bị alias
  • Những ý tưởng giống iso permission của Pony, hoặc quyền tạm thời chỉ cho phép nhìn vào bên trong struct nhưng không cho dùng tham chiếu trỏ ra bên ngoài, cũng vẫn là các khả năng đang được cân nhắc
  • Phần khó là duy trì được sự linh hoạt này trong khi vẫn giữ các mục tiêu của Ante là tính dễ dùng, tính dễ đọc và sự đơn giản

Xu hướng rộng hơn của an toàn bộ nhớ

  • Quan điểm nền tảng là shared mutable borrowing trước đây từng bị xem là bất khả thi, và Rust cũng được thiết kế dựa trên niềm tin đó
  • Nhưng ngày càng có nhiều ngoại lệ tích lũy lại
    • Ante có thể lấy tham chiếu mượn uniq từ dữ liệu shared-mutable thông qua quy tắc local uniqueness
    • Vale có thể lấy tham chiếu mượn bất biến từ dữ liệu shared-mutable thông qua pure function
    • group borrowing có thể tạo tham chiếu mượn shared-mutable ngay cả khi không shape-stable
    • GhostCell của Rust cho phép các đồ thị đối tượng tự do trỏ vào nhau, nhưng tại một thời điểm cụ thể chỉ được có một tham chiếu khả biến tới một trong số chúng
  • Xu hướng này gợi ý rằng có thể tồn tại một nguyên lý tổng quát hơn để xử lý shared mutable borrowing trong thiết kế an toàn bộ nhớ

So sánh với Cell của Rust

  • Người dùng Rust có thể đặt câu hỏi về khác biệt giữa cách này và cách đặt Cell vào trường của struct
  • Trong ví dụ của Ante, có thể lấy tham chiếu mut String tới status: String từ Rc Spaceship và nối trực tiếp " (refueling)"
  • Với cách Cell<String> trong Rust, không thể lấy &mut String từ Rc<Spaceship>
    • Thay vào đó phải dùng status_ref.replace(String::new()) để chèn một giá trị mặc định tạm thời
    • sửa String đã lấy ra
    • rồi cuối cùng dùng lại replace(status) để đưa nó trở lại
  • Cách này có một số nhược điểm
    • Phải tạo một thể hiện mặc định như ""
    • Có nguy cơ quên lời gọi replace cuối cùng
    • Có nguy cơ ai đó đọc status khi giá trị vẫn đang ở trạng thái đã bị thay thế
  • Ante cho phép tạm thời lấy tham chiếu tới chuỗi status, đồng thời trình biên dịch sẽ ép buộc rằng trong lúc đó mã khác không thể truy cập vào nó

Bài viết liên quan

1 bình luận

 
GN⁺ 4 giờ trước
Ý kiến trên Lobste.rs

  • Việc từng cho rằng “shared mutable borrow” là bất khả thi không chỉ đơn thuần là sự đánh đổi mà Rust chấp nhận để đạt mục tiêu, mà gần như chính là mục tiêu cốt lõi của Rust
    Bởi trạng thái khả biến được chia sẻ khiến việc suy luận cục bộ về mã trở nên khó khăn
    "References are like jumps" của withoutboats nói rất hay về điểm này. Việc ngăn trạng thái có bí danh bị thay đổi ngoài ý muốn là chìa khóa để dễ xây dựng hệ thống hoạt động đúng, và có lập luận rằng các quy tắc lifetime của Rust không chỉ là cơ chế để tránh garbage collection, mà là một cấu trúc sâu hơn nhằm đảm bảo khả năng suy luận trong ngôn ngữ cho phép đồng thời trạng thái khả biến và trạng thái có bí danh

    • Trước đây khi tác giả bàn về Mojo borrow checker tôi cũng đã nghĩ như vậy. Borrow checker của Rust giúp duy trì ngữ nghĩa giá trị ngay cả trong chương trình đơn luồng

  • Trông khá ổn
    Nếu tôi hiểu đúng, phép màu chuyển từ tham chiếu chia sẻ sang tham chiếu khả biến là khả thi vì nó bị giới hạn ở các kiểu không được chia sẻ giữa các luồng, và tính duy nhất của Rc dường như được đảm bảo bằng cách coi mọi đối tượng cùng kiểu như được mượn với cùng một lifetime
    Việc thích cú pháp tường minh hay cú pháp tự nhiên có thể là vấn đề sở thích, nhưng điều này cho thấy nếu compiler biết nhiều hơn về Cell thì có thể cho phép tham chiếu khả biến tới nó linh hoạt hơn
    Đồng thời cũng tránh được cách dùng từ gây nhầm lẫn trong Rust, nơi mut được dùng theo nghĩa độc quyền/duy nhất chứ không phải khả biến

    • Tôi từng thắc mắc chuyện này sẽ ra sao giữa các luồng. Kiểu như “việc nâng cấp uniq có nghĩa là phải lấy khóa không?” nhưng có vẻ ý ở đây là đang so với Rc chứ không phải Arc
    • Bạn có thể giải thích thêm chỗ mut mang nghĩa độc quyền/duy nhất được không?

  • Tôi tò mò không biết có ai đoán ra được nguyên lý hợp nhất mà phần cuối bài viết gợi ý là gì không

  • Các thảo luận trước đây về bài blog trên antelang.org cũng đáng xem

  • Tôi không thật sự hiểu cách này hoạt động. Có vẻ như nó nói rằng “nếu bạn có con trỏ khả biến tới một đối tượng thì bạn có thể lấy được tham chiếu thay đổi tới một lát cắt của đối tượng đó”
    Nhưng nếu vậy thì dường như sẽ có thể làm kiểu mutref someobjext = …, mutref subfield = someobjext.a.b, someobjext.a = somethingelse, và khi đó subfield có thể bị vô hiệu hóa hoặc hỏng do giá trị bị thay đổi
    Bài viết có nhiều giải thích, so sánh với ngôn ngữ khác và ví dụ mã, nhưng lại khó tìm thấy phần thật sự trình bày ngữ nghĩa từng bước của cơ chế này một cách cơ bản