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
Add OM for pthread_rwlock_rdlock #1516
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for submitting this PR, @Anthonysdu.
Can I also ask you to add a regression test that gives "VERIFICATION FAILED"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Lgtm
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Many thanks, @Anthonysdu.
b60d8f1
to
8d11468
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, thanks!
Thanks for submitting this PR, @Anthonysdu. |
The regression testcase is a reduced version from the incorrect false of
read_write_lock-1-pthread
in SVCOMP.From the pthread document:
The calling thread acquires the write lock if no other thread (reader or writer) holds the read-write lock rwlock.
The calling thread acquires the read lock if a writer does not hold the lock and there are no writers blocked on the lock.