Charly
LightNews LightNews
banner
charlycst.bsky.social
Charly
@charlycst.bsky.social
23 followers 62 following 25 posts
Computer system researcher, working on OS, virtualization, and confidential computing.
Posts Replies Media Videos
charlycst.bsky.social
The new `unsafe_op_in_unsafe_fn` warning in #rust 2024 is good in general, but for small functions with a single expression it creates a lot of unnecessary indentation... It would be cool if it were allowed to add `unsafe` in front of a `match` or `if` to reduce indentation in those cases.
A match expression with the unsafe keyword in front. Not currently allowed by Rust. ```rs unsafe match (vaddr, asid) { (None, None) => asm!("sfence.vma"), (None, Some(asid)) => asm!( "sfence.vma x0, {asid}", asid = in(reg) asid, ), ... } ```
October 23, 2025 at 3:34 PM
charlycst.bsky.social
Packing for SOSP 2025!
A bunch of stickers of the Miralis logo.
October 10, 2025 at 10:40 PM
charlycst.bsky.social
Those last few weeks I have been working on translating the RISC-V spec into Rust. The compiler can't handle the full spec just yet, but I have an initial prototype with support for the full RISC-V decoder and physical memory protection.

Here is the repo for the curious: github.com/CharlyCst/so...
A Rust code snippet that demonstrates how to interact with the Rust translation of the RISC-V spec. This example showcase how to check if a memory access will pass physical memory protection. ```rust let mut core = new_core(config::U74); let addr = 0x8000_0000; let access_kind = AccessType::Read(()); // By default M-mode can access all memory assert!(core.pmp_check(addr, access_kind).is_none()); // But U-mode will get an access fault core.set_mode(Privilege::User); assert_eq!( core.pmp_check(addr, access_kind), Some(ExceptionType::E_Load_Access_Fault(())), ); ```
June 17, 2025 at 8:36 AM
charlycst.bsky.social
Tomorrow I am flying to Alberta to attend HotOS, I will be presenting our work on lightweight hypervisor verification.

In a nutshell, we translated the RISC-V spec to Rust (with an in-house Sail-to-Rust transpiler), and used the Kani model checker to verify key components of Miralis.
A snippet of code to verify the implementation of `mret` emulation in the Miralis virtual firmware monitor. The function first create two symbolic contexts (i.e. where all registers are symbolic, that is they can be arbitrary values), and execute the `mret` instruction with both the Miralis instruction emulator and the reference Sail RISC-V model. If the resulting symbolic contexts are equal, the Miralis implementation is correct for all possible inputs. ```rust /// Verify the emulation of the `mret` instruction. #[cfg_attr(kani, kani::proof)] pub fn check_mret() { let (mut ctx, mut mctx, mut sail_ctx) = symbolic::new_symbolic_contexts(); ctx.emulate_mret(&mut mctx); // Miralis implementation execute_MRET(&mut sail_ctx); // Sail implementation assert_eq!( ctx, adapters::sail_to_miralis(sail_ctx, &mctx), "mret instruction emulation is not correct" ); } ```
May 11, 2025 at 9:49 PM
charlycst.bsky.social
We just received the new HiFive P550, a tiny bit too late for Christmas.
Time to try out this H extension!
A picture of the HiFive P550 development board
January 10, 2025 at 10:13 AM
charlycst.bsky.social
Those days I am reading "The Art of Doing Science And Engineering" by Richard Hamming, the book was published in 1997 but it is astonishing how clearly he was reading into the future in so many aspects.
What will come along to sustain this straight line logarithmic growth curve and prevent the inevitable flattening out of the S-curve of applications? The next big area is, I believe, pattern recognition. I doubt our ability to cope with the most general problem of pattern recognition, because for one thing it implies too much, but in areas like speech recognition, radar pattern recognition, picture analysis and redrawing, workload scheduling in factories and offices, analysis of data for statisticians, creation of virtual images, and such, we can consume a very large amount of computer power.
December 8, 2024 at 10:04 PM