Library Ergonomics

[toolCHAINZ]

Over the years there's been a few distinct but related ergonomics issues raised about this library:

• The ctx lifetime can be unwieldy to work with (just my own observation) and tends to infect anything that has to use z3
• Nothing is sendable, limiting the library's usability for those needing multithreaded support (Aren't Config, Context, Solver and friends Send-able? #100, [WIP] Send for SendableContext (unsafe, but clearly marked as unsafe) #102, Add a safe way to interrupt computation from another thread #122). I myself have run into this and ended up just fully reconstructing my formulas in separate threads.
• There is no "default" context like there is in the python bindings (Use an "implicit" Context? #261)

All three of these prevent users from doing things that "feel like they should work" and lead to a lot of juggling of context references. I propose the following incremental plan to address these:

Step 1 : Eliminate 'ctx with a reference-counted context handle

Context can be refactored as follows (pseudocode follows):

struct ContextInternal{
   _ctx: Z3_context
}

impl Drop for ContextInternal{
   // insert the current Context Drop impl
}

#[derive(Clone)]
struct Context{
   _ctx: Rc<ContextInternal>
}

All Ast and Solver instances can now own ctx, fully removing the 'ctx lifetime.

This would be a breaking change, obviously.

I think ContextHandle could be left unchanged with this implementation, as it could still use a 'ctx lifetime referring to the original Context instance that spawned it. That is conservative (since the lifetime of each individual Context handle is <= that of the ContextInternal) and sound.

The main benefit here would be removing the 'ctx lifetime from all the Ast structs. Reads of Rc have ~0 overhead over & references. Clone and Drop have some small overhead due to the refcount, but it should be very minimal, and I think it's worth the tradeoff.

Step 2: Thread-local Default Contexts

We should do what @waywardmonkeys recommended in #261. I personally would probably lean towards having the "default context" methods get the shorter names. So BV::from_u64 would use the default thread-local Context and we can introduce BV::from_u64_with_ctx that allows providing a Context. These could be automatically defined with a macro. Alternatively, continuing our BV example, maybe we introduce (also with a macro) a ContextBV type that takes a context on all -> Self methods and is Into<BV> to avoid cluttering the BV type.

Or maybe we make an opinionated stance and say "no actual user should be using more than one context per thread".

Not sure what approach makes the most sense here but I think the ergonomic benefit from this change would be huge. This would also allow for trait implementations like From<bool> for Bool and From<u64> for BV.

With this change, combined with Step 1, this library becomes almost identical to the Python bindings in overall ergonomics.

Step 3: Opinionated multi-threading

We make the addition I suggested in #100 (comment):

• Context stays !Send and !Sync. Context can still then use an Rc.
• Everything other than Context gets (through traits/macros) a -Sendable variant which is Send but !Sync and !Clone. These variants would use a temporary Context which is inaccessible outside the type (and thus safely sendable to another thread), and internally use a translate call to copy the original C++ object for the temporary Context. The only methods on constructed values of these types are translate() and translate_ctx(ctx), which allow for producing the original Ast/Solver struct, with the underlying Z3 object translated into the thread default Context or the specified Context respectively.

The main drawback with this method I see is in performance of moves across threads (due to creating contexts and the 2x translate call). On my machine it takes a couple milliseconds to create a Context. It would be possible to use this "improperly" and see a big slowdown (e.g. making 10000 Bools in thread A and send them to thread B makes 10000 temporary Contexts). However, for use-cases I anticipate as common, I think this would be minimal overhead (e.g. making 1000 assertions in a solver and sending it to another thread creates 1 temporary Context).

This has a few advantages:

• I think this is clearly sound (double-checking and pushback if it's not is certainly welcome)
• This makes no compromise on single-threaded usage performance; no arc/mutex type stuff is getting added.
• This actually makes the ergonomics of the rust bindings better than python, because python has nothing stopping you from moving an Ast to the wrong thread and using it with its original context, which can lead to difficult-to-track memory corruption errors.

Any thoughts about all this @waywardmonkeys @Pat-Lafon?

[toolCHAINZ]

I made a PR to quickly try out the first idea here: #401

As a consumer of this library who puts a lot of Asts and Solvers into structs, being able to get rid of the 'ctx lifetime would be a quality-of-life improvement for me.

This is a pretty big change though so I wouldn't want to do this unilaterally. If I get some time I'd like to do a proper benchmark of this, but some initial tests show no significant performance degredation:

=====================================================
// 'cargo test' on #401
Executed in    1.88 secs    fish           external
   usr time    1.30 secs    9.35 millis    1.29 secs
   sys time    0.74 secs    3.05 millis    0.74 secs

Executed in    2.54 secs    fish           external
   usr time    1.23 secs    0.09 millis    1.23 secs
   sys time    0.89 secs    1.41 millis    0.89 secs

Executed in    2.26 secs    fish           external
   usr time    1.23 secs    0.09 millis    1.23 secs
   sys time    0.74 secs    1.30 millis    0.74 secs

Executed in    1.90 secs    fish           external
   usr time    1.30 secs    0.14 millis    1.30 secs
   sys time    0.74 secs    1.75 millis    0.74 secs



=====================================================
// 'cargo test' on master 
Executed in    2.38 secs    fish           external
   usr time    1.24 secs    0.14 millis    1.24 secs
   sys time    0.78 secs    1.45 millis    0.78 secs

Executed in    1.76 secs    fish           external
   usr time    1.24 secs    0.08 millis    1.24 secs
   sys time    0.72 secs    1.43 millis    0.72 secs

Executed in    2.34 secs    fish           external
   usr time    1.26 secs    0.08 millis    1.26 secs
   sys time    0.78 secs    1.01 millis    0.78 secs

Executed in    2.36 secs    fish           external
   usr time    1.27 secs    0.14 millis    1.27 secs
   sys time    0.78 secs    1.68 millis    0.78 secs

[Pat-Lafon]

Ok, I slightly miss-understood that in some cases you would still be passing around a Context object(because of the impl case you described) but I think my thought here is still valid.

[toolCHAINZ]

Regarding the context lifetime:

I thought a little more about this and it really doesn't provide any guarantees about mixing Asts from different contexts. You're totally free to write something like this:

fn main() {
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let ctx2 = Context::new(&cfg);
    let a = Bool::from_bool(&ctx, false);
    let ab = Bool::from_bool(&ctx2, true);
    panicky(a, ab);
}

fn panicky<'ctx>(a: Bool<'ctx>, b: Bool<'ctx>) {
    let _panic = a._eq(&b); //panics
}

I think the lifetimes here might give users an impression of safety against this, but if a user is doing something with multiple contexts it would still be possible for them to mess it up; if the lifetimes overlap, there's no safeguard against mixing them.

That's true, if someone were to hold on to an Ast or something while dropping everything else the context would hang around. Agreed it seems niche, I am having trouble thinking of a case where that would realistically happen. Hopefully such a "leak" wouldn't be that bad either, as it would just be that one Ast and the context itself kept around and everything else using the Context would still be freed on Drop. The context object itself is not that large, especially on the scale of how much memory solvers use.

[toolCHAINZ]

I think I'm going to go ahead with this change. I ported my existing code to this branch as a test. The port was fairly easy and I was able to remove so many lifetimes while also greatly simplifying some trait implementations and callback-based code that was mired in lifetimes before. I also (anecdotally) didn't observe any slowdowns.

[toolCHAINZ]

Thanks for the comments!

[toolCHAINZ]

#401 has been merged!

[Pat-Lafon]

I was looking at the dependents of the rust Z3 bindings(https://crates.io/crates/z3/reverse_dependencies) and to be fair, not many of them seem to be up-to-date/well-maintained(so not very representative). On one hand, crates like LibAFL and such might have more complex Z3 usage that ordinary users don't(But actually in looking at their code, they do everything in one function so there are no lifetime parameters involved at all.). Looking at biodivine-lib-param-bn, they don't seem to be doing anything too fancy but are representative of what you are talking about where lifetimes just infect a few data structures/functions without much benefit. They do use an iterator pattern for going through different satisfying models(Seems like, negating out different combinations of bools and getting new models) which I think will be covered by models reference counting the context.

[Pat-Lafon]

I'm not sure if Step2 is more focused on the thread_local part or the bifurcating of the API. You could do the former without the latter like you mention.

For thread_local versus Rc. What does that change for the user? The API has one less parameter with a thread local, some things that are currently methods on Context would need to be stand-alone functions(As in no ctx.update_param_value but instead Context::update_param_value), though figuring out how to juggle multiple contexts seems harder with thread_local. I'm not sure if this changes you send/translate API?

For bifurcating the API, I think ContextBV could be cleaner since you would then be hiding away the context methods for auto-complete and such which seems nice. Though, don't most of the non-c/c++ official language bindings hide away the Z3 context without issue? Maybe it's not worth maintaining 2 API versions(or a non-trivial macro system).

[toolCHAINZ]

I just had a thought. I saw @waywardmonkeys mentioned using a scoped context and I'd never really considered it but that might be very clean.

Perhaps instead of the macro system, we:

• Get rid of the macro and have only default ctx variants of APIs.
• Keep the thread local refcell context
• Add something like z3::with_context(ctx, || {}) and/or z3::with_config(cfg, || {}) which accepts a context (or a config with which to build one) and swaps the thread local out with the new one for the duration of the execution of the closure.

This would be a structured way of working with multiple contexts that should be difficult to misuse. Since everything is Rc'd there's no memory safety danger swapping things out. We could even mark the closures as Send and Sync to force the user to translate any incoming Asts into the closure with the Synchronized API. It would be difficult or impossible to mix z3 objects from different ctxs then.

My only concern is that I've done a bit of cross-FFI work with this library before that involved some foreign contexts and I'm not sure if this would be flexible enough for that (very niche) use case.

[Pat-Lafon]

Hmm, that's interesting. It would be nice to only need one variant. I wasn't sure about AST's moving in and out but your comment about them being Send/Sync would handle that.

Taking your latter comment into account. I guess the question is, who are these multiple or non-default context API's for? My guess is that their use is somewhat niche compared to just the thread local context. Maybe if we had the clear-er use case, it would make this tradeoff more clear(Or I don't have enough experience with this setup to tell the difference).

[toolCHAINZ]

I gave the scoped idea a try and it works nicely. Currently just fixing up the tests and then I'll be pushing up a version with just that, the thread local stuff, and no macro. I think I'll be comfortable merging that version.

I had to delete a few tests for mixing contexts because there's not a way to express them now, which seems like a good sign.

Agreed, idk exactly what case someone would want to use these. I'm fine moving forward with the closure-based strategy and if that's not flexible enough for whoever needs it we can deal with that later.

I'm leaving the wrap methods as-is (including a context arg) so my own niche cross-FFI case isn't a concern for me. I think that gives me enough to work with.

[toolCHAINZ]

Ok yeah, I finished fixing this up and pushed it. I'm feeling even better about it now. These API changes mean that I could simplify the trait setup for converstions (e.g. bv + 4). There's now a single IntoAst trait, which sorts like BV and Float implement directly. Other types that don't need additional context to form a sort just implement From and then get IntoAst through a blanket impl.

I'll plan on merging this version today.

[toolCHAINZ]

#417 is merged! I'm going to close this discussion now, as I think the outstanding "ergonomic" issues here are solved. The only other big breaking change I'm tracking is the NonNull/Result stuff, but that's separate.

[Pat-Lafon]

I don't have much of an opinion for multi-threading. For a few reasons, if I want parallelism, I turn my constraints into a smtlib file and pass it off to z3 in it's own process(So clearly making some overhead sacrifices)(Note you can also get parallelism within Z3 by setting a parameter).

Either way, a clear example of doing multi-threading with Z3, maybe using rayon or async(I'm not sure which would make more sense) would be cool to see.

[toolCHAINZ]

Yeah I can definitely see the benefits of doing it that way.

In my own case, I ran into the ergonomic paper cut where what I wanted to do was to build a set of formulas in the main thread, clone them into worker threads, and then use message passing to communicate the results of queries, and eventually to return an SMT Model back to the main thread.

Instead, I had to sort of artificially split up the API of my consuming code and ship a Send structure to each thread that had all the information needed to build the formulas, and then build copies in each thread. Instead of returning a model, I then had to return metadata about how it was constructed back to the original thread to then allow it to re-run a solver and get a model.

Being able to just do the following would have cleaned up a lot of code:

• Make a big Vec of Asts at the start of the algorithm and send them to a thread
• Just directly return the Model from the worker thread and translate it for the main thread

I hadn't considered usage with Rayon or async but that would definitely be interesting. I think both rayon and tokio at least are work stealing so that might be difficult to get working properly, but it would be cool! I guess only -Sendable structures would be allowed in either method, so maybe it would just lead to some extra translation overhead.

[toolCHAINZ]

I did a simple proof-of-concept implementation of my idea and it seems to work. I also thought of a way to avoid making contexts in the (I think common) case that a user wants to ship something like a Vec of Asts over.

I have a trait-based system for producing the "Sendable" structs, with macro-based implementations for z3 rs types. I also have an auto implementation for Vec<T> where T is an Ast and can translate. I think this should enable most cases where a user wants to bulk send some Asts to another thread without needing to make one context per ast.

I also expose the (unsafe) traits and structures used so that a user can implement them for their own types. There's some invariants they need to uphold (they must construct the structure with a context not held elsewhere, and they must ONLY use that context), hence the unsafe. I'll make another PR for that following the refcount stuff.

[toolCHAINZ]

I made a draft PR of this idea (#404), I think it is fairly clean and should be difficult to misuse.

I don't have an urgent need for this so I'll probably leave it as is for a bit and not merge it just yet, but I think this is a promising direction

[toolCHAINZ]

I'm not good at "leaving things for a bit" apparently. I worked on this some more, consulted with upstream Z3 on the safety of the approach, and now have this code in a state that I'm happy with it. I'll be merging it shortly.