+/**
+ Properties to check:
+ 1. At most 1 thread can acquire the write lock, and at the same time, no
+ other threads can acquire any lock (including read/write lock).
+ 2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
+ 3. A read_unlock release 1 read lock, and a write_unlock release the write
+ lock. They can not release a lock that they don't acquire.
+ ###
+ 4. Read_lock and write_lock can not be grabbed at the same time.
+ 5. Happpens-before relationship should be checked and guaranteed, which
+ should be as the following:
+ a. read_unlock hb-> write_lock
+ b. write_unlock hb-> write_lock
+ c. write_unlock hb-> read_lock
+*/
+
+/**
+ Interesting point for locks:
+ a. If the users unlock() before any lock(), then the model checker will fail.
+ For this case, we can not say that the data structure is buggy, how can we
+ tell them from a real data structure bug???
+ b. We should specify that for a specific thread, successful locks and
+ unlocks should always come in pairs. We could make this check as an
+ auxiliary check since it is an extra rule for how the interfaces should called.
+*/
+
+/** @DeclareState: bool writerLockAcquired;
+ int readerLockCnt; */
+
+int read_can_lock(rwlock_t *lock)