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

CI: heapster-tests take a mysteriously long time to complete #1843

Closed
RyanGlScott opened this issue Mar 16, 2023 · 1 comment
Closed

CI: heapster-tests take a mysteriously long time to complete #1843

RyanGlScott opened this issue Mar 16, 2023 · 1 comment
Labels
performance Issues that involve or include performance problems subsystem: heapster Issues specifically related to memory verification using Heapster tooling: CI Issues involving CI/CD scripts or processes

Comments

@RyanGlScott
Copy link
Contributor

The heapster-tests CI job takes approximately 2 hours to complete at the moment, which is even longer than it takes to run the awslc job. See a recent example of this here. What's more, I don't have a keen sense as to why this happens. If you look at the log from that job, it does report some timing info for certain Coq commands:

Tactic call is_elem_spec_ref ran for 6.178 secs (3.542u,0.089s) (success)
COQC mbox_proofs.v
File "./mbox_proofs.v", line 10, characters 0-44:
Warning: Notation "_ ~= _" was already used. [notation-overridden,parsing]
Warning: Admitting the bitvector proposition below if it holds for w <= 3
(forall (w : nat) (a b : bitvector w), bvAdd w a (bvSub w b a) = b)
Warning: Admitting the bitvector proposition below if it holds for w <= 3
(forall (w : nat) (a b c : bitvector w),
 isBvule w c b -> isBvule w a (bvSub w b c) -> isBvule w a b)
Warning: Admitting the bitvector proposition below if it holds for w <= 3
(forall (w : nat) (x y : bitvector w),
 isBvult w y x ->
 isBvult w (bvSub w x (bvAdd w y (intToBv w 1))) (bvSub w x y))
Tactic call
mbox_free_chain_spec_ref ran for 1.44 secs (1.412u,0.027s) 
(success)
Finished transaction in 2.068 secs (2.068u,0.s) (successful)
Tactic call mbox_concat_spec_ref ran for 0.544 secs (0.54u,0.004s) (success)
Finished transaction in 1.022 secs (1.022u,0.s) (successful)
Tactic call
mbox_concat_chains_spec_ref__dec_args ran for 19.948 secs (19.73u,0.215s) 
(success)
Finished transaction in 20.38 secs (20.332u,0.043s) (successful)
Tactic call
mbox_concat_chains_spec_ref__fuel ran for 17.149 secs (16.935u,0.211s) 
(success)
Finished transaction in 18.155 secs (18.153u,0.s) (successful)
Tactic call mbox_detach_spec_ref ran for 0.429 secs (0.429u,0.s) (success)
Finished transaction in 0.781 secs (0.779u,0.s) (successful)
Tactic call mbox_drop_spec_ref ran for 2.868 secs (2.868u,0.s) (success)
Finished transaction in 3.408 secs (3.408u,0.s) (successful)
Tactic call
mbox_len_spec_ref__dec_args ran for 6.733 secs (6.732u,0.s) 
(success)
Finished transaction in 5.322 secs (5.322u,0.s) (successful)
Tactic call mbox_len_spec_ref__fuel ran for 6.665 secs (6.664u,0.s) (success)
Finished transaction in 5.314 secs (5.313u,0.s) (successful)
Tactic call mbox_copy_spec_ref ran for 7.116 secs (7.1u,0.015s) (success)
Finished transaction in 26.413 secs (26.4u,0.007s) (successful)
Tactic call
mbox_copy_chain_spec_ref ran for 18.594 secs (18.592u,0.s) 
(success)
Tactic call
mbox_split_at_spec_ref ran for 22.566 secs (22.366u,0.195s) 
(success)
Tactic call
mbox_detach_from_end_spec_ref ran for 1.978 secs (1.977u,0.s) 
(success)
Tactic call
mbox_randomize_spec_ref ran for 14.588 secs (14.586u,0.s) 
(success)

But none of them actually take that long. This suggests that something else is taking up the bulk of the time. We should track down what this is at try to reign it in, or at the very least, add some additional logging to make it obvious that it is the thing that takes up so much time.

@RyanGlScott RyanGlScott added performance Issues that involve or include performance problems tooling: CI Issues involving CI/CD scripts or processes subsystem: heapster Issues specifically related to memory verification using Heapster labels Mar 16, 2023
@eddywestbrook
Copy link
Contributor

Closed by #1928

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
performance Issues that involve or include performance problems subsystem: heapster Issues specifically related to memory verification using Heapster tooling: CI Issues involving CI/CD scripts or processes
Projects
None yet
Development

No branches or pull requests

2 participants