Skip to content
This repository has been archived by the owner on Aug 20, 2021. It is now read-only.

Use wall-clock time in timeouts #384

Open
asymmetric opened this issue Mar 30, 2020 · 0 comments
Open

Use wall-clock time in timeouts #384

asymmetric opened this issue Mar 30, 2020 · 0 comments
Labels
enhancement New feature or request

Comments

@asymmetric
Copy link
Contributor

[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.

timeout uses either timer_create(2) or alarm(2), depending on the result of this check.

When timer_create is used, it's called with CLOCK_REALTIME, which in theory should do what we want, i.e. measure wall-clock time.

I haven't been able to figure out whether alarm tracks 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 alarm and 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.

@asymmetric asymmetric added the enhancement New feature or request label Mar 30, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant