elliottt / easy-smt

Easy SMT solver interaction
Apache License 2.0
24 stars 7 forks source link

Resource temporarily unavailable (os error 35) when called too many times in MacOS #26

Closed Qi-Zhan closed 6 months ago

Qi-Zhan commented 6 months ago

Hello, I'm using easy-smt in my project, which will call ContextBuilder::new().solver("z3", ["-smt2", "-in"]).build(); too many times and I found Resource temporarily unavailable (os error 35) occur. For example

use easy_smt::ContextBuilder;

fn main() {
    let mut i = 0;
    loop {
        let ctx = ContextBuilder::new().solver("z3", ["-smt2", "-in"]).build();
        match ctx {
            Ok(_) => {
                i += 1;
                println!("Success: {}", i);
            }
            Err(e) => {
                eprintln!("Failed to create context: {}", e);
            }
        }
    }
}
Success: 2269
Success: 2270
Success: 2271
Success: 2272
Success: 2273
Success: 2274
Success: 2275
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Success: 2276
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)
Failed to create context: Resource temporarily unavailable (os error 35)

It returns error when i is 1000+/2000+. I think it might be related to process creatation.

Any help or suggestion would be appreciated.

fitzgen commented 6 months ago

easy-smt spawns a subprocess for every context you create, so I'd look at your configured user process limits. For example, on linux:

$ ulimit -u
Qi-Zhan commented 6 months ago

ulimit -u
2666

Now I understand the reason, thanks