[nix-shell:~/temp/k-uniswap-v2]# time klab prove --dump --timeout 3d
...
/root/temp/foo/deps/klab/evm-semantics/deps/k/k-distribution/target/release/k/bin/../lib/k: line 7: 54551 CPU time limit exceeded (core dumped) java -Dfile.encoding=UTF-8 -Djava.awt.headless=true -Xms64m -Xmx4096m -Xss32m -XX:+TieredCompilation -Xmx10G -ea -cp "/root/temp/k-uniswap-v2/deps/klab/evm-semantics/deps/k/k-distribution/target/release/k/lib/java/*" org.kframework.main.Main "$@"
Proof TIMEOUT: 6f14fa919d6fb0ead618f33fcf23efafd81bc87a465a14adeb7b81b78d15c323.k [Foo_bar_pass_rough] (with state logging)
real 621m39.410s
user 4318m26.121s
sys 17m56.192s
As can be seen above, the timeout didn't expire after 3 days of wall-clock time. Instead, it used CPU time, multiplied by the cores in use by the process on the machine (4318m ≈ 3 days).
I think it would be more intuitive if wall-clock time were used.
Currently, klab-prove uses timeout to set timeouts on kprove.
As can be seen above, the timeout didn't expire after 3 days of wall-clock time. Instead, it used CPU time, multiplied by the cores in use by the process on the machine (4318m ≈ 3 days).
I think it would be more intuitive if wall-clock time were used.
Currently, klab-prove uses
timeoutto set timeouts on kprove.timeoutuses eithertimer_create(2)or alarm(2), depending on the result of this check.When
timer_createis used, it's called withCLOCK_REALTIME, which in theory should do what we want, i.e. measure wall-clock time.I haven't been able to figure out whether
alarmtracks CPU or wall-clock time (the man page isn't clear about this, and I couldn't find the source).So either we're using
alarmand it tracks CPU time, or I've misunderstood something along the way.For reference, the uutils/coreutils Rust re-implementation of coreutils implements timeouts like this.