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

[BUG] Extremely slow checking of apparently simple OpenSUT code #124

Open
2 of 4 tasks
peterohanley opened this issue Sep 25, 2024 · 2 comments
Open
2 of 4 tasks
Labels
CN Issues related to the CN tool

Comments

@peterohanley
Copy link
Collaborator

Summary

Adding a few more specs to the OpenSUT (trying to work around lack of accesses in declaration specs) has resulted in code that takes a very long time to check. I don't know how long because it hasn't finished but more than an hour. Before I added these specs it was taking about 90s.

Bug

Noticed on

% cn --version
git-9a71b713c [2024-09-12 00:45:26 +0100]

Appears still present on

% cn --version
git-98434f0d7 [2024-09-25 18:54:24 +0100]
# this is HEAD of branch 11-implement-mps currently
git checkout e2be19d6417b7cbb6f0dbd9f608e3085669fe8c3
cd components/mission_protection_system/src
make -f cn.mk -k -j4 components/actuation_unit.cn

Acceptance Criteria

CN accepts or rejects this code much faster. I would like to know what behavior caused this performance crash but a mine like this in the tool is very bad.

Do

  • assign issue to a Milestone
  • define acceptance criteria
  • add appropriate labels
  • Update this section to based on the Acceptance Criteria
@peterohanley peterohanley added the CN Issues related to the CN tool label Sep 25, 2024
@podhrmic
Copy link
Collaborator

The commit leading to the poor performance is GaloisInc/VERSE-OpenSUT@e2be19d

@peterohanley
Copy link
Collaborator Author

Reduced to rems-project/cerberus#613

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

No branches or pull requests

2 participants