search

Baltoli / project-docs

Documents for my Part III project
0 stars 0 forks source link

FF...T Analysis #31

Closed Baltoli closed 7 years ago

Baltoli commented 7 years ago

Implement the analysis that ensures the proper sequence of return values is observed by the lock acquire function.

Baltoli commented 7 years ago

Put this on hold as a) it's more complex than the other analyses, and b) I haven't got an example that shows why it's needed yet. It may even be the case that it's not necessary, as the other analyses are strict enough to catch it.

Baltoli commented 7 years ago

Actually, this is needed to detect multiple acquisition attempts.