Skip to content

Commit

Permalink
Implement Concurrency6 package -- split out Concurrency7
Browse files Browse the repository at this point in the history
  • Loading branch information
MichaelRFairhurst committed Nov 1, 2024
1 parent 041150a commit fb3c5e7
Show file tree
Hide file tree
Showing 33 changed files with 1,125 additions and 59 deletions.
39 changes: 6 additions & 33 deletions c/cert/src/rules/CON39-C/ThreadWasPreviouslyJoinedOrDetached.ql
Original file line number Diff line number Diff line change
Expand Up @@ -14,37 +14,10 @@

import cpp
import codingstandards.c.cert
import codingstandards.cpp.Concurrency
import codingstandards.cpp.rules.joinordetachthreadonlyonce.JoinOrDetachThreadOnlyOnce

// OK
// 1) Thread calls detach parent DOES NOT call join
// 2) Parent calls join, thread does NOT call detach()
// NOT OK
// 1) Thread calls detach, parent calls join
// 2) Thread calls detach twice, parent does not call join
// 3) Parent calls join twice, thread does not call detach
from C11ThreadCreateCall tcc
where
not isExcluded(tcc, Concurrency5Package::threadWasPreviouslyJoinedOrDetachedQuery()) and
// Note: These cases can be simplified but they are presented like this for clarity
// case 1 - calls to `thrd_join` and `thrd_detach` within the parent or
// within the parent / child CFG.
exists(C11ThreadWait tw, C11ThreadDetach dt |
tw = getAThreadContextAwareSuccessor(tcc) and
dt = getAThreadContextAwareSuccessor(tcc)
)
or
// case 2 - multiple calls to `thrd_detach` within the threaded CFG.
exists(C11ThreadDetach dt1, C11ThreadDetach dt2 |
dt1 = getAThreadContextAwareSuccessor(tcc) and
dt2 = getAThreadContextAwareSuccessor(tcc) and
not dt1 = dt2
)
or
// case 3 - multiple calls to `thrd_join` within the threaded CFG.
exists(C11ThreadWait tw1, C11ThreadWait tw2 |
tw1 = getAThreadContextAwareSuccessor(tcc) and
tw2 = getAThreadContextAwareSuccessor(tcc) and
not tw1 = tw2
)
select tcc, "Thread may call join or detach after the thread is joined or detached."
class ThreadWasPreviouslyJoinedOrDetachedQuery extends JoinOrDetachThreadOnlyOnceSharedQuery {
ThreadWasPreviouslyJoinedOrDetachedQuery() {
this = Concurrency5Package::threadWasPreviouslyJoinedOrDetachedQuery()
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
c/common/test/rules/joinordetachthreadonlyonce/JoinOrDetachThreadOnlyOnce.ql
74 changes: 67 additions & 7 deletions c/common/test/includes/standard-library/stdatomic.h
Original file line number Diff line number Diff line change
@@ -1,9 +1,69 @@
#define atomic_compare_exchange_weak(a, b, c) 0
#define atomic_compare_exchange_weak_explicit(a, b, c, d, e) 0
#define atomic_load(a) 0
#define atomic_load_explicit(a, b)
#define atomic_store(a, b) 0
#define atomic_store_explicit(a, b, c) 0
#define ATOMIC_VAR_INIT(value) (value)
#define atomic_is_lock_free(obj) __c11_atomic_is_lock_free(sizeof(*(obj)))
typedef _Atomic(int) atomic_int;
typedef _Atomic(int) atomic_int;

#define __ATOMIC_RELAXED 0
#define __ATOMIC_CONSUME 1
#define __ATOMIC_ACQUIRE 2
#define __ATOMIC_RELEASE 3
#define __ATOMIC_ACQ_REL 4
#define __ATOMIC_SEQ_CST 5

typedef enum memory_order {
memory_order_relaxed = __ATOMIC_RELAXED,
memory_order_consume = __ATOMIC_CONSUME,
memory_order_acquire = __ATOMIC_ACQUIRE,
memory_order_release = __ATOMIC_RELEASE,
memory_order_acq_rel = __ATOMIC_ACQ_REL,
memory_order_seq_cst = __ATOMIC_SEQ_CST
} memory_order;

void atomic_thread_fence(memory_order);
void atomic_signal_fence(memory_order);

#define atomic_thread_fence(order) __c11_atomic_thread_fence(order)
#define atomic_signal_fence(order) __c11_atomic_signal_fence(order)

#define atomic_store(object, desired) __c11_atomic_store(object, desired, __ATOMIC_SEQ_CST)
#define atomic_store_explicit __c11_atomic_store

#define atomic_load(object) __c11_atomic_load(object, __ATOMIC_SEQ_CST)
#define atomic_load_explicit __c11_atomic_load

#define atomic_exchange(object, desired) __c11_atomic_exchange(object, desired, __ATOMIC_SEQ_CST)
#define atomic_exchange_explicit __c11_atomic_exchange

#define atomic_compare_exchange_strong(object, expected, desired) __c11_atomic_compare_exchange_strong(object, expected, desired, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)
#define atomic_compare_exchange_strong_explicit __c11_atomic_compare_exchange_strong

#define atomic_compare_exchange_weak(object, expected, desired) __c11_atomic_compare_exchange_weak(object, expected, desired, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)
#define atomic_compare_exchange_weak_explicit __c11_atomic_compare_exchange_weak

#define atomic_fetch_add(object, operand) __c11_atomic_fetch_add(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_add_explicit __c11_atomic_fetch_add

#define atomic_fetch_sub(object, operand) __c11_atomic_fetch_sub(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_sub_explicit __c11_atomic_fetch_sub

#define atomic_fetch_or(object, operand) __c11_atomic_fetch_or(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_or_explicit __c11_atomic_fetch_or

#define atomic_fetch_xor(object, operand) __c11_atomic_fetch_xor(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_xor_explicit __c11_atomic_fetch_xor

#define atomic_fetch_and(object, operand) __c11_atomic_fetch_and(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_and_explicit __c11_atomic_fetch_and

typedef struct atomic_flag { _Atomic(_Bool) _Value; } atomic_flag;

_Bool atomic_flag_test_and_set(volatile atomic_flag *);
_Bool atomic_flag_test_and_set_explicit(volatile atomic_flag *, memory_order);

void atomic_flag_clear(volatile atomic_flag *);
void atomic_flag_clear_explicit(volatile atomic_flag *, memory_order);

#define atomic_flag_test_and_set(object) __c11_atomic_exchange(&(object)->_Value, 1, __ATOMIC_SEQ_CST)
#define atomic_flag_test_and_set_explicit(object, order) __c11_atomic_exchange(&(object)->_Value, 1, order)

#define atomic_flag_clear(object) __c11_atomic_store(&(object)->_Value, 0, __ATOMIC_SEQ_CST)
#define atomic_flag_clear_explicit(object, order) __c11_atomic_store(&(object)->_Value, 0, order)
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
// GENERATED FILE - DO NOT MODIFY
import codingstandards.cpp.rules.joinordetachthreadonlyonce.JoinOrDetachThreadOnlyOnce

class TestFileQuery extends JoinOrDetachThreadOnlyOnceSharedQuery, TestQuery { }
File renamed without changes.
24 changes: 24 additions & 0 deletions c/misra/src/rules/DIR-5-2/NotNoDeadlocksBetweenThreads.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
/**
* @id c/misra/not-no-deadlocks-between-threads
* @name DIR-5-2: There shall be no deadlocks between threads
* @description Circular waits leading to thread deadlocks may be avoided by locking in a predefined
* order.
* @kind problem
* @precision very-high
* @problem.severity error
* @tags external/misra/id/dir-5-2
* external/misra/c/2012/amendment4
* correctness
* concurrency
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.cpp.rules.preventdeadlockbylockinginpredefinedorder.PreventDeadlockByLockingInPredefinedOrder

class NotNoDeadlocksBetweenThreadsQuery extends PreventDeadlockByLockingInPredefinedOrderSharedQuery {
NotNoDeadlocksBetweenThreadsQuery() {
this = Concurrency6Package::notNoDeadlocksBetweenThreadsQuery()
}
}
29 changes: 29 additions & 0 deletions c/misra/src/rules/DIR-5-3/BannedDynamicThreadCreation.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
/**
* @id c/misra/banned-dynamic-thread-creation
* @name DIR-5-3: There shall be no dynamic thread creation
* @description Creating threads outside of a well-defined program start-up phase creates
* uncertainty in program behavior and concurrency overhead costs.
* @kind problem
* @precision low
* @problem.severity error
* @tags external/misra/id/dir-5-3
* external/misra/c/2012/amendment4
* external/misra/c/audit
* correctness
* maintainability
* concurrency
* performance
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.cpp.Concurrency

from CThreadCreateCall tc, Function enclosingFunction
where
not isExcluded(tc, Concurrency6Package::bannedDynamicThreadCreationQuery()) and
enclosingFunction = tc.getEnclosingFunction() and
not enclosingFunction.getName() = "main"
select tc, "Possible dynamic creation of thread outside initialization in function '$@'.",
enclosingFunction, enclosingFunction.toString()
45 changes: 45 additions & 0 deletions c/misra/src/rules/DIR-5-3/ThreadCreatedByThread.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
/**
* @id c/misra/thread-created-by-thread
* @name DIR-5-3: Threads shall not be created by other threads
* @description Creating threads within threads creates uncertainty in program behavior and
* concurrency overhead costs.
* @kind problem
* @precision high
* @problem.severity error
* @tags external/misra/id/dir-5-3
* external/misra/c/2012/amendment4
* correctness
* maintainability
* concurrency
* performance
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.cpp.Concurrency

Function callers(Function f) { result = f.getACallToThisFunction().getEnclosingFunction() }

class ThreadReachableFunction extends Function {
/* The root threaded function from which this function is reachable */
Function threadRoot;

ThreadReachableFunction() {
exists(CThreadCreateCall tc |
tc.getFunction() = callers*(this) and
threadRoot = tc.getFunction()
)
}

/* Get the root threaded function from which this function is reachable */
Function getThreadRoot() { result = threadRoot }
}

from CThreadCreateCall tc, ThreadReachableFunction enclosingFunction, Function threadRoot
where
not isExcluded(tc, Concurrency6Package::threadCreatedByThreadQuery()) and
enclosingFunction = tc.getEnclosingFunction() and
threadRoot = enclosingFunction.getThreadRoot()
select tc, "Thread creation call reachable from threaded function '$@'.", threadRoot,
threadRoot.toString()
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
/**
* @id c/misra/atomic-aggregate-object-directly-accessed
* @name RULE-12-6: Structure and union members of atomic objects shall not be directly accessed
* @description Accessing a member of an atomic structure or union results in undefined behavior.
* @kind problem
* @precision very-high
* @problem.severity error
* @tags external/misra/id/rule-12-6
* external/misra/c/2012/amendment4
* correctness
* concurrency
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra

from Expr expr, Field field
where
not isExcluded(expr, Concurrency6Package::atomicAggregateObjectDirectlyAccessedQuery()) and
not expr.isUnevaluated() and
(
exists(FieldAccess fa |
expr = fa and
fa.getQualifier().getUnderlyingType().hasSpecifier("atomic") and
field = fa.getTarget()
)
or
exists(PointerFieldAccess fa |
expr = fa and
fa.getQualifier().getUnderlyingType().(PointerType).getBaseType().hasSpecifier("atomic") and
field = fa.getTarget()
)
)
select expr, "Invalid access to member '$@' on atomic struct or union.", field, field.getName()
Loading

0 comments on commit fb3c5e7

Please sign in to comment.