rems-project / isla

Symbolic execution tool for Sail ISA specifications
Other
61 stars 9 forks source link

The usage of lifetimes ('ir) makes moving tasks, frames and localframes impossible #17

Open Trolldemorted opened 3 years ago

Trolldemorted commented 3 years ago

I see that you have one big lifetime that enforces the shared state stays alive as long as the frames and tasks do. Since that makes using those types significantly more cumbersome and impairs the potential to embed them into larger frameworks, I have begun to replace them with owning pointers.

Was there a specific reason you went for references, or would you like to merge that change upstream? Right now it is not completely finished, but it works well enough to run my kernel until it pops from the stack into PC. I can't yet fully estimate what parts of your codebase I am breaking, so I'd love to hear your opinion early on.

Alasdair commented 3 years ago

I use &T because it's the simplest 'right' pointer type in some sense, as we have some immutable shared data (the intermediate representation we are executing) that is being accessed my multiple threads concurrently. Arc would imply some additional synchronization cost whenever it's created, cloned, or dropped. It'd be nice to see an example where plain references are more cumbersome.

All the 'ir lifetime enforces is that you don't drop the code you are executing before you're finished with it. Switching from &'ir T to Arc<T> in SharedState implies changing the ownership pattern so initialize_architecture consumes (takes ownership) of the IR syntax tree so that every shared state can have shared ownership of bits of it via Arcs. From that point on we only every access the syntax tree via SharedState so that probably isn't problematic.

However I think we probably still want to use a plain reference in UVal, and in this new setting the reference here would need to share the same lifetime as the pointer to the shared_state, so Frame and LocalFrame would still have lifetime parameters (but the lifetime would be shorter, which might just make the ownership less clear). I suspect using Arc here would be quite inefficient - I have been thinking of changing Arc<Memory<B>> into &'ir Memory<B> (borrow checker permitting) for this reason.

Trolldemorted commented 3 years ago

Arc would imply some additional synchronization cost whenever it's created, cloned, or dropped.

Do you have any benchmarks I can run to assert whether the change has any measurable impact? The difference between passing a ref and cloning an Arc should only be an atomic increment/decrement of the refcount (which targets a memory range which will be in the L1 cache). I have been running my kernel as far as it can, and the execution times in both isla-lib variants (vanilla and my PR) were not significantly diverging (~6.7 seconds for both according to a few manually done runs with Measure-Command { cargo run --bin test --release }). My PR is still a rather dirty hack, I didn't evaluate which Arc clones could be replaced by &* yet, so the Arc clone/drop overhead could be reduced.

It'd be nice to see an example where plain references are more cumbersome.

You can't have functions that load an architecture, so this does not compile because the resulting architecture depends on values owned by the stack frame:

fn load_arch<'ir>() -> (Vec<Def<Name, B64>>,
    Symtab<'ir>, ISAConfig<B64>) {
    let now = Instant::now();
    let folder = PathBuf::from(r"C:\Users\Benni\repositories\master\verification\sail-arm\1166c197b127ed30d95421dcfa5fc59716aa1368");
    //let folder = PathBuf::from(r"C:\Users\Benni\Downloads\");
    //let folder = PathBuf::from(r"C:\Users\Benni\repositories\master-arm\aarch64");
    let config_file = folder.join("aarch64.toml");
    let symtab_file = folder.join("aarch64.symtab");
    let ir_file     = folder.join("aarch64.irx");

    let strings: Vec<String> = bincode::deserialize(&fs::read(&symtab_file).unwrap()).unwrap();
    let symtab = Symtab::from_raw_table(&strings);
    let mut ir: Vec<Def<Name, B64>> = ir_serialize::deserialize(&fs::read(&ir_file).unwrap()).expect("Failed to deserialize IR");
    let isa_config: ISAConfig<B64> = ISAConfig::parse(&fs::read_to_string(&config_file).unwrap(), &symtab).unwrap();
    println!("Loaded architecture in: {}ms", now.elapsed().as_millis());
    (ir, symtab, isa_config)
}

In general you can't move anything in that lifetime dependency tree as long as a leaf depends on it. However, everything in that dependency tree is immutable, so Rust's shared immutable ownership patters really fit in well here.

Also you cannot move tasks into a lazy_static hashmap (because the hashmap may live longer than SharedState):

lazy_static! {
    static ref HASHMAP: HashMap<u32, Task<B64>> = { // Task requires lifetime, lazy_static forbids lifetime
        HashMap::new()
    };
}

This makes it impossible to gather tasks/frames in a lazy_static place, which I would otherwise do (one of my goals is to speed up execution by deriving transformation functions and applying these to the memory/registers instead of symbolically re-executing frequent blocks again and again).

I expect other dependents to have esoteric needs as well, imo you should impose as few lifetimes as possible on your consumers, because they will definitely find a way to shoot themselves in the foot with them.

All the 'ir lifetime enforces is that you don't drop the code you are executing before you're finished with it. Switching from &'ir T to Arc in SharedState implies changing the ownership pattern so initialize_architecture consumes (takes ownership) of the IR syntax tree so that every shared state can have shared ownership of bits of it via Arcs. From that point on we only every access the syntax tree via SharedState so that probably isn't problematic.

That's exactly what I have been doing in #18 : initialize_architecture consumes the arch (Vec<Def<Name, B>>), and Frame.instrs is now a Arc<Vec<Instr<Name, B>>> instead of &'ir [Instr<Name, B>].

However I think we probably still want to use a plain reference in UVal, and in this new setting the reference here would need to share the same lifetime as the pointer to the shared_state, so Frame and LocalFrame would still have lifetime parameters (but the lifetime would be shorter, which might just make the ownership less clear). I suspect using Arc here would be quite inefficient - I have been thinking of changing Arc<Memory<B>> into &'ir Memory<B> (borrow checker permitting) for this reason.

Could you elaborate why you'd prefer Uninit(Arc<Ty<Name>>) over Uninit(&'ir Ty<Name>)? If performance is your primary concern, I could try to create some benchmarks which could confirm or refute our assumptions about the performance impact. Do Uninits occur frequently in your use cases? After going through executor.rs I assumed they are only placeholders for symbols (because as soon as they are used they are being replaced by unconstrained symbols), so I expected they will be ousted by symbols quickly, and have no significant on the overall performance.

Alasdair commented 3 years ago

You can't have functions that load an architecture, so this does not compile because the resulting architecture depends on values owned by the stack frame:

It does force loading an architecture to be a two step process, but it's something you typically only do once so I'm not sure it's really important?

Also you cannot move tasks into a lazy_static hashmap (because the hashmap may live longer than SharedState):

For this you can use Box::leak on the loaded architecture to upgrade it's lifetime to 'static. If what you want is a static global intermediate representation so every lifetime becomes static this is probably the way to go, something like:

static ARCH_SRC: &str = include_str!("../aarch64.ir");

lazy_static! {
    static ref ARCH_UNINTERNED: &'static [Def<String, B64>] = {
        let lexer = lexer::Lexer::new(ARCH_SRC);
        let arch = ir_parser::IrParser::new().parse(lexer).unwrap_or_else(|_| Vec::new());
        Box::leak(arch.into_boxed_slice())
    };
    static ref ARCH: (&'static [Def<Name, B64>], Symtab<'static>) = {
        let mut symtab = Symtab::new();
        let arch = symtab.intern_defs(&ARCH_UNINTERNED);
        (Box::leak(arch.into_boxed_slice()), symtab)
    };
}
Alasdair commented 3 years ago

Oh I should mention I'm pretty busy today working on some slides for tomorrow, I'll be able to give some more complete replies when I don't have to do that!

Trolldemorted commented 3 years ago

It does force loading an architecture to be a two step process, but it's something you typically only do once so I'm not sure it's really important?

That depends on what users are doing downstream. There are very weird systems out there, including ones with different processors sharing the same memory and whatnot, so I would not assume consumers won't want to load/unload architectures in their validation pipelines.

For this you can use Box::leak on the loaded architecture to upgrade it's lifetime to 'static. If what you want is a static global intermediate representation so every lifetime becomes static this is probably the way to go, something like:

Those are nice hacks indeed, I didn't realize one can abuse leak to achieve static lifetimes! But still, I strive to have code which has the least possible WTFs/minute, and rust's shared ownership fat pointers innately model your use case quite nicely :( As I said if you are worried about performance I can try to set up some benchmarks, the atomic inc/decrement of the refcount really shouldn't have a real impact on the execution time.

Oh I should mention I'm pretty busy today working on some slides for tomorrow, I'll be able to give some more complete replies when I don't have to do that!

No problem, good luck with your presentation!