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

Introduce stdlib.cat #751

Merged
merged 4 commits into from
Oct 10, 2024
Merged

Introduce stdlib.cat #751

merged 4 commits into from
Oct 10, 2024

Conversation

hernanponcedeleon
Copy link
Owner

In herd, most of what we defined in basic.cat is defined in stdlib.cat which is included by default in all models (see section 16.7 in https://diy.inria.fr/doc/herd.html).

This PR mimics this behavior.

@ThomasHaas
Copy link
Collaborator

We did not always place the stdlib include at the beginning, for example in vmm.cat. The default include might cause issue in that regard. Well, I guess you can re-include the stdlib.cat after modifying definitions to overwrite the already created one's.

@hernanponcedeleon
Copy link
Owner Author

I thought about that, and I still decided to remove it to see if this already causes problems. I assume the vmm.cat from the libvsync repo should not depend on another cat files so this probably will need to be fixed in the official model. I will discuss that with jonas.

@ThomasHaas
Copy link
Collaborator

The failed checks even include the RelationAnalysisTest. That means you just exposed some more bugs in RA or AA I think.

Signed-off-by: Hernan Ponce de Leon <[email protected]>
@hernanponcedeleon
Copy link
Owner Author

The failed checks even include the RelationAnalysisTest. That means you just exposed some more bugs in RA or AA I think.

Maybe it is the non-det from #746 and this was just an unlucky run.

@ThomasHaas
Copy link
Collaborator

But the non-det was supposed to only affect the new alias analysis which is disabled inRelationAnalysisTest. So if it is non-det behaviour, then you exposed it on the older versions of AA.

Signed-off-by: Hernan Ponce de Leon <[email protected]>
@hernanponcedeleon
Copy link
Owner Author

hernanponcedeleon commented Oct 10, 2024

I thought about that, and I still decided to remove it to see if this already causes problems. I assume the vmm.cat from the libvsync repo should not depend on another cat files so this probably will need to be fixed in the official model. I will discuss that with jonas.

The latest version of vmm already solves most of the issues, it only need to properly define po-loc

EDIT: we don't need to redefine po-loc since it does not depends on the new ext and int

Copy link
Collaborator

@ThomasHaas ThomasHaas left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@hernanponcedeleon hernanponcedeleon merged commit c828b96 into development Oct 10, 2024
1 check passed
@hernanponcedeleon hernanponcedeleon deleted the stdlib branch October 10, 2024 16:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants