search

Baltoli / project-docs

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

Release Reachable #39

Closed Baltoli closed 7 years ago

Baltoli commented 7 years ago

From a true acquire return (in the FF...T analysis), we should check that it is possible to reach a call to release OR a call to a releasing function. This will exclude incorrect analyses such as:

if(lock_acquire(&lock)) {
  return;
}

while(!lock_acquire(&lock)) {}
lock_release(&lock);

being analysed as OK - we can see that this definitely isn't OK as there's no static way to reach either event described above.