Summary: `ReentrantReadWriteLock.ReadLock` and `ReentrantReadWriteLock.WriteLock` are commonly used lock types that were not previously modeled. Reviewed By: peterogithub Differential Revision: D4262032 fbshipit-source-id: 4ff81a7master
parent
826accc21b
commit
c1205c1453
@ -0,0 +1,146 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
package codetoanalyze.java.checkers;
|
||||
|
||||
import java.util.concurrent.locks.Lock;
|
||||
import java.util.concurrent.locks.ReadWriteLock;
|
||||
import java.util.concurrent.locks.ReentrantLock;
|
||||
import java.util.concurrent.locks.ReentrantReadWriteLock;
|
||||
|
||||
@ThreadSafe
|
||||
public class Locks {
|
||||
|
||||
Integer f;
|
||||
|
||||
Lock mLock;
|
||||
ReadWriteLock mReadWriteLock;
|
||||
ReentrantLock mReentrantLock;
|
||||
ReentrantReadWriteLock mReentrantReadWriteLock;
|
||||
|
||||
public void lockInOneBranchBad(boolean b) {
|
||||
if (b) {
|
||||
mLock.lock();
|
||||
}
|
||||
f = 24;
|
||||
if (b) {
|
||||
mLock.unlock();
|
||||
}
|
||||
}
|
||||
|
||||
public void afterUnlockBad() {
|
||||
mLock.lock();
|
||||
mLock.unlock();
|
||||
f = 42;
|
||||
}
|
||||
|
||||
public void afterReentrantLockUnlockBad() {
|
||||
mReentrantLock.lock();
|
||||
mReentrantLock.unlock();
|
||||
f = 42;
|
||||
}
|
||||
|
||||
public void afterWriteLockUnlockBad() {
|
||||
mReentrantReadWriteLock.writeLock().lock();
|
||||
mReentrantReadWriteLock.writeLock().unlock();
|
||||
f = 42;
|
||||
}
|
||||
|
||||
public void lockOk() {
|
||||
mLock.lock();
|
||||
f = 42;
|
||||
mLock.unlock();
|
||||
}
|
||||
|
||||
public void lockBothBranchesOk(boolean b) {
|
||||
if (b) {
|
||||
mLock.lock();
|
||||
} else {
|
||||
mLock.lock();
|
||||
}
|
||||
f = 42;
|
||||
mLock.unlock();
|
||||
}
|
||||
|
||||
public void reentrantLockOk() {
|
||||
mReentrantLock.lock();
|
||||
f = 42;
|
||||
mReentrantLock.unlock();
|
||||
}
|
||||
|
||||
public void rReentrantLockTryLockOk() {
|
||||
if (mReentrantLock.tryLock()) {
|
||||
f = 42;
|
||||
mReentrantLock.unlock();
|
||||
}
|
||||
}
|
||||
|
||||
public void reentrantLockInterruptiblyOk() throws InterruptedException {
|
||||
mReentrantLock.lockInterruptibly();
|
||||
f = 42;
|
||||
mReentrantLock.unlock();
|
||||
}
|
||||
|
||||
private void acquireLock() {
|
||||
mLock.lock();
|
||||
}
|
||||
|
||||
public void acquireLockInCalleeOk() {
|
||||
acquireLock();
|
||||
f = 42;
|
||||
mLock.unlock();
|
||||
}
|
||||
|
||||
public void writeLockOk() {
|
||||
mReadWriteLock.writeLock().lock();
|
||||
f = 42;
|
||||
mReadWriteLock.writeLock().unlock();
|
||||
}
|
||||
|
||||
public void reentrantWriteLockOk() {
|
||||
mReentrantReadWriteLock.writeLock().lock();
|
||||
f = 42;
|
||||
mReentrantReadWriteLock.writeLock().unlock();
|
||||
}
|
||||
|
||||
private void releaseLock() {
|
||||
mLock.unlock();
|
||||
}
|
||||
|
||||
// our "squish all locks into one" abstraction is not ideal here...
|
||||
public void FP_unlockOneLock() {
|
||||
mLock.lock();
|
||||
mReentrantLock.lock();
|
||||
mReentrantLock.unlock();
|
||||
f = 42;
|
||||
mLock.unlock();
|
||||
}
|
||||
|
||||
// ... or here
|
||||
public void FN_releaseLockInCalleeBad() {
|
||||
mLock.lock();
|
||||
releaseLock();
|
||||
f = 42;
|
||||
}
|
||||
|
||||
// we don't model the case where `tryLock` fails
|
||||
public void FN_withReentrantLockTryLockBad() {
|
||||
if (!mReentrantLock.tryLock()) {
|
||||
f = 42;
|
||||
}
|
||||
}
|
||||
|
||||
// we shouldn't be able to write when holding a readLock
|
||||
public void FN_readLockOk() {
|
||||
mReentrantReadWriteLock.readLock().lock();
|
||||
f = 42;
|
||||
mReentrantReadWriteLock.readLock().unlock();
|
||||
}
|
||||
|
||||
}
|
@ -0,0 +1,22 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
package codetoanalyze.java.checkers;
|
||||
|
||||
import java.lang.annotation.Documented;
|
||||
import java.lang.annotation.ElementType;
|
||||
import java.lang.annotation.Retention;
|
||||
import java.lang.annotation.RetentionPolicy;
|
||||
import java.lang.annotation.Target;
|
||||
|
||||
@Documented
|
||||
@Target(ElementType.TYPE)
|
||||
@Retention(RetentionPolicy.CLASS)
|
||||
public @interface ThreadSafe {
|
||||
}
|
@ -1,9 +1,10 @@
|
||||
codetoanalyze/java/threadsafety/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
|
||||
codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
|
||||
codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
|
||||
codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
|
||||
codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_unlockOneLock(), 4, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 1, THREAD_SAFETY_ERROR, [call to void ThreadSafeExample.assignInPrivateMethodOk(),access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.deeperTraceBad(), 1, THREAD_SAFETY_ERROR, [call to void ThreadSafeExample.callAssignInPrivateMethod(),call to void ThreadSafeExample.assignInPrivateMethodOk(),access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ThreadSafeExample.f]
|
||||
|
Loading…
Reference in new issue