-
Notifications
You must be signed in to change notification settings - Fork 42
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
replaying a built-in returned a different result than expected #77
Comments
Thanks for the bug report! The problem here is the call to Concuerror should of course report this limitation and not crash. I will write a patch for this, but it will not really make the particular test work, just fail in a better way. |
Thanks @aronisstav ! this is test with
|
Indeed, but it shouldn't. It should have the same problem. |
Stateless systematic testing requires that any state of the program that has already been visited can be reached again just by making the same scheduling choices. In order for this to work, one must control all other sources of nondeterminism. NIFs unfortunately cannot, in general, be guaranteed to return the same result for each call with the same arguments. With this patch Concuerror aborts attempts to run code that is loading NIFs. Fixes parapluu#77.
Stateless model checking requires that any state of the program can reliably be reached just by making the same scheduling choices. In order for this to work, one must control all other sources of nondeterminism. NIFs cannot, in general, be guaranteed to return the same result for each call with the same arguments, nor can they be detected/intercepted. With this patch Concuerror emits a warning when instrumenting modules that may try to load NIFs. Fixes parapluu#77.
With this patch Concuerror will emits a warning when instrumenting modules that may try to load NIFs. NIFs cannot, in general, be guaranteed to return the same result for each call with the same arguments, nor can they be detected/intercepted. Stateless model checking requires that any state of the program can reliably be reached just by making the same scheduling choices. In order for this to work, one must control all other sources of nondeterminism. Fixes parapluu#77.
With this patch Concuerror will emits a warning when instrumenting modules that may try to load NIFs. NIFs cannot, in general, be guaranteed to return the same result for each call with the same arguments, nor can they be detected/intercepted. Stateless model checking requires that any state of the program can reliably be reached just by making the same scheduling choices. In order for this to work, one must control all other sources of nondeterminism. Fixes parapluu#77.
I got this error message while running concurerror
The text was updated successfully, but these errors were encountered: