T-spec meeting 2024-02-08

--- title: T-spec meeting 2024-02-08 tags: ["T-spec", "meeting", "minutes"] date: 2024-02-08 discussion: https://rust-lang.zulipchat.com/#narrow/stream/399173-t-spec/topic/Meeting.202024-02-08 url: https://hackmd.io/ffNlEA5ERUSY2DGeg1qvUg --- *Note: Meeting was set 5 hours later than the normal start time.* Attendees: Joel Marcey, Connor Horman, Pietro, Eric Huss, Mara Bos, TC, JF Bastien, Mario Carneiro, Lukas Wirth, Walter Pearce, Felix ## Potential Agenda - Safety Critical Rust and the specification with Woven by Toyota - Specification Chapter Structure - Any Other Business ## Safety Critical Rust and the Specification JF kicked things off with an introduction People may know JF from his work on C++ and wants to talk about the specification. JF is working at Woven by Toyota and on loan to Toyota as a consultant. Platform infrastructure team for a group of suppliers that come together. They write safety critical software for automotive. The issue being faced is that C/C++ is the path taken for this type of software, but they are not necessarily safety critical. No one will prevent bad code in a car from being shipped. But they will come when something bad happens. They are currently using standards like MISRA. Rust is a good solution for safety critical software. Needs the ecosystem, tooling, etc. to get automotive to buy into it. ISO-26262 describes safety standards for automotive. Aviation, for example, has different standards. "MISRA for Rust" would be fairly small. There needs to be an industry group to push forward the adoption of Rust. It needs to be more than one automaker or one team or person within an organization. Specificaiton in and of itself is definitely a good thing, but it would also be good to be able to have the specificaiton check the boxes for safety critical - e.g., similar to what Ferrocene does for the toolchain. JF's vision for this is that the Rust Foundation could support and be a venue for the people and organizations that need to come together to advance safety-critical Rust. Working with IEEE on a new standard. C/C++ memory model is the de facto specification that other languages forked and modified over time. C/C++ memory model has a formal proof of correctness. Implemented in LLVM and gcc. C++ abstract machine is effectively a standard. Rust forked the standard in the past but may have kept (fixed?) the broken pieces. He would like for the abstract machine standard to be housed in IEEE, and he's working to get the copyrights assigned to make this possible. This means if you are writing a specification for a language, then you can utilize the abstract memory model machine and describe how that works for your language, subset or otherwise. Three types of instructions: Memory instrucutions, control instructions and arithmetic instructions. Rust should continue working on the specification with an eye towards maybe importing the abstract memory model. This could allow to more easily find defects. Felix recommends that JF discuss this with Ralf Jung who has been working on memory model work. Mario: Ralf's work is not conering atomic memory model stuff - still borrowing from C. Connor: Recommends that JF reach out directly to the opsem team maybe as opposed to directly to Ralf. Eric: What is the timeline for this over the next year? JF: Cares most about advancing the safety side. It would be useful to start contacting others in the automative industry. JF: Design Automation conference may be a good place to discuss this. JF: On the abstract machine standard, that will take longer. Memory model stuff would be 3-4 years, even if you punt on other work. Joel: How could our current work for the specification coincide with a potential 3-4 year runway for the abstract memory model machine? JF: Thinking through the idea of an abstract machine while we work on the specificaiton will be a good exercise even as we wait for the memory model standard. Mario: This will come up when we start specifying FFI and LTO anyway. This could be language agnostic anyway. Joel: We have not really talked about a memory model in the Rust specification yet. We have room to manuever on how we want to approach it. JF: C++ memory model has a lot of holes in areas around shared memory, arithmetic types. TC: This would be a great discussion to have with the opsem team. Their work, in a sense, once adopted by the lang team, forms the actual operational semantics of Rust, and the spec team is a consumer of that. Mario: The only member of the opsem team here. Work on MiniRust could be applicable here. We may not have the specification of floating point, etc. immediately. There are a lot of areas where it is difficult to know where we are going. TC: Popping the stack a bit here, JF had mentioned two other items we might discuss: 1) how can a specification help with adoption of Rust in safety-critical applicatinos, and 2) what role can the Foundation play in bringing together industry partners? Pietro: For safety critical you need a list of requirements. For a compiler, that is what the language does. You don't need to specify what the borrow checker does. Need to balance starting from scratch vs. needs of where industry/vendors is moving now. TC: JF, what are the gaps beteween what work has been done with Ferrocene and the fact that you are not yet using Rust for safety critical systems? JF: Having only one entity using a thing makes it hard to make traction when others in the industry haven't adopted it yet. We need to have collaboration across the industry and have a good spec. Pietro: Rust is doing better than other languages/toolchains because the Rust Project already does most of the work for safety critical, other than the "paperwork". TC: JF, what are the concrete deliverables you would be looking to see, and how would we know if we were moving forward? JF: Would like to end up with a fairly well agreed upon a "good" subset of Rust with tools that are enforced. This includes brining in part of the ecosystem, maybe a subset of Cargo. Bring in safety levels that are agreed upon by those in the industry that would utilize the certification. But wants to do this without an imposition on the community. TC: Joel, what are your thoughts on how the Foundation might be able to help here? Joel: I can see the Foundation having something called the "Safety Critical Initiative" that allows the Foundation to be an umbrella entity to allow these conversations to happen across various companies that care about Safety Critical Rust. Mario: If Rust is collaborating with IEEE on a common memory model. Is the copyright going to cause issues? What would JF like to see out of this meeting? JF: Memory model informative. But would like to get moving on a consortium for safety crticial. (The meeting ended here.) ## Specification Chapter Structure Saved for next meeting.