Linux Driver Verification » Linux Kernel Safety RuleDB

A reader-writer lock is a spinlock, except you lock it in one of two modes: a `read lock' or a `write lock'. More than one people can share a `read lock', but the write lock is exclusive: if someone has a write lock, no one can have any lock.

• - multiple write locks are not permitted
  - multiple write unlocks are not permitted

• - read lock is not permitted after write lock

• - read unlock is not permitted before read lock
  - write unlock is not permitted before write lock

• - read and write locks must be free at the end