Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mark self as mut borrow in solver methods? #266

Open
108anup opened this issue Nov 2, 2023 · 4 comments
Open

Mark self as mut borrow in solver methods? #266

108anup opened this issue Nov 2, 2023 · 4 comments

Comments

@108anup
Copy link
Contributor

108anup commented Nov 2, 2023

I am new to rust, but I noticed that the functions like Solver::assert borrow an immutable reference to self. Should these be annotated as mutable given that such functions modify the solver object. If not, could you please explain the rationale behind it.

pub fn assert(&self, ast: &ast::Bool<'ctx>) {
    ///       ^^^^^ Here
    debug!("assert: {:?}", ast);
    unsafe { Z3_solver_assert(self.ctx.z3_ctx, self.z3_slv, ast.z3_ast) };
}
@Pat-Lafon
Copy link
Contributor

I think this is best described as the Interior Mutability Pattern since all objects are secretly reference counted on the Z3 c side of things.

@108anup
Copy link
Contributor Author

108anup commented Nov 2, 2023

Okay, I guess the reference counting can ensure memory leaks are absent. But that may not protect against race conditions, right?

For example, one might borrow a solver for its model in a closure. Then one might update the solver assertions, and then query the closure. If now the closure is called, then the result is for the updated solver.

The onus is then on the user to ensure that such things don't happen. There are no compile-time or run-time checks for this, right? If the annotation is made mutable, then such behaviors would not be allowed by the compiler. What is the benefit of keeping the annotation immutable?

In the above example, the closure could just borrow the model and not the solver to avoid any inconsistency. But ideally IMO, the compiler should force the user to do this and this should not be a choice because isn't such safety the whole point of rust, otherwise one might as well use C++.

@waywardmonkeys
Copy link
Contributor

IIRC, the underlying C++ code is already thread safe which is why we were able to remove the Z3_MUTEX that existed in earlier versions of the code.

If you start to use &mut self, you also make it harder to use some of this from multiple threads (which I think some people do or did do...)

@Pat-Lafon
Copy link
Contributor

How does one write this program? I'm not super familiar with threads so more for my own benefit. So I think almost all of the major structures in the z3 crate are !Send and !Sync because raw pointers are one of the exceptions for auto-deriving these(https://doc.rust-lang.org/nomicon/send-and-sync.html). Thus you can't just trivially pass a reference into a spawned thread without a compiler error.

You can isolate everything into it's own thread, but that seems safe to me anyways given z3's guarantees here.

use std::{
    thread::{self, sleep},
    time::Duration,
};

use z3::{
    ast::{Ast, Int},
    Config, Context, Solver,
};

fn main() {
    let mut handles = Vec::new();
    for _ in 0..5 {
        let handle = thread::spawn(move || {
            let cfg = &Config::new();
            let ctx = Context::new(cfg);
            let x = Int::new_const(&ctx, "x");
            let solver = Solver::new(&ctx);
            sleep(Duration::from_secs(1));
            solver.assert(&x._eq(&x));
            sleep(Duration::from_secs(1));
            solver.check();
        });
        handles.push(handle);
    }

    for t in handles.into_iter() {
        t.join().unwrap();
    }

    println!("Hello, world!");
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants