Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
107 changes: 88 additions & 19 deletions src/transitions/cond/MCCondWait.cpp
Original file line number Diff line number Diff line change
@@ -1,28 +1,109 @@
#include "mcmini/transitions/cond/MCCondWait.h"
#include "mcmini/MCTransitionFactory.h"
#include "mcmini/mcmini_private.h"
#include "mcmini/mcmini_private.h" /* For trace_pid, and state */
#include "mcmini/transitions/mutex/MCMutexLock.h"
#include "mcmini/transitions/mutex/MCMutexTransition.h"
#include "mcmini/misc/cond/MCConditionVariableArbitraryPolicy.hpp"
#include <pthread.h>
#include <string.h>
#include <sys/uio.h> /* For process_vm_readv() */

MCTransition *
MCReadCondWait(const MCSharedTransition *shmTransition, void *shmData,
MCStack *state)
{
// In theory, we should never see an undefined PTHREAD_COND_INITIALIZER.
// src/transitions/cond/MCReadCondEnqueue.cpp should trigger first.
const auto shmCond =
static_cast<MCSharedMemoryConditionVariable *>(shmData);
const auto condInShm = shmCond->cond;
const auto mutexInShm = shmCond->mutex;
const auto condSystemId = (MCSystemID)condInShm;
pthread_cond_t * condSystemId = *static_cast<pthread_cond_t **>(shmData);
// We can't freeze this as 'const', since we might have to init cond later.
const auto mutexSystemId = (MCSystemID)mutexInShm;
const auto condThatExists =
// We can't freeze this as 'const', since we might have to init cond later.
auto condThatExists =
state->getVisibleObjectWithSystemIdentity<MCConditionVariable>(
condSystemId);
const auto mutexThatExists =
state->getVisibleObjectWithSystemIdentity<MCMutex>(mutexSystemId);

MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
condThatExists != nullptr, "Attempting to wait on a condition "
"variable that is uninitialized");
bool testIfValidCond = false;
// SEE: src/transitions/cond/MCCondInit.cpp:MCReadCondInit()
if (condThatExists == nullptr) {
auto shadow = MCConditionVariable::Shadow(condSystemId);
// If this has state 'undefined', then the condThatExists is still 'NULL'
if (shadow.state == MCConditionVariable::Shadow::undefined) {
testIfValidCond = true;
}
// FIXME: Allow dynamic selection of wakeup policies.
// For now, we hard-code it here. Not great, but at least
// we can change it relatively easily still

// FIXME: We're assigning a condition variable policy of arbitrary.
// Is this reasonable?
auto policy = std::unique_ptr<mcmini::ConditionVariablePolicy>(
new mcmini::ConditionVariableArbitraryPolicy());

auto newCond =
std::make_shared<mcmini::ConditionVariable>(shadow, std::move(policy));
// Then create and register an MCConditionVariable object.
state->registerVisibleObjectWithSystemIdentity(condSystemId, newCond);
// condThatExists =
// std::static_pointer_cast<MCConditionVariable, MCVisibleObject>(
// newCond);
// Get the current cond var on the stack, along with condSystemIdentity
// (the pthread_cond_t struct of the user).
condThatExists =
state->getVisibleObjectWithSystemIdentity<MCConditionVariable>(
condSystemId);
#if 0
// This is an alternative.
condThatExists =
std::static_pointer_cast<MCConditionVariable, MCVisibleObject>(newCond);
#endif
// This is still MCConditionVariable::Shadow::undefined;
// We set that in the next 'if' statement.
}

if (testIfValidCond || condThatExists -> shadow.state ==
MCConditionVariable::Shadow::undefined) {
#ifdef HAS_PROCESS_VM
pthread_cond_t cond_initializer = PTHREAD_COND_INITIALIZER;
// NOTE: If PTHREAD_COND_INITIALIZER was used on a global variable,
// the macro is all zeros, and the data segment is all zeros.
// So, we can't tell if the initializer was or was not used.
// But if a local variable of type pthread_cond_t is not
// not initialized with PTHREAD_COND_INITIALIZER, and was
// not initialized with pthread_cond_init, then this code can
// truly catch an error. pthread_cond_signal() would return
// error "Illegal argument", but only if the user had checked
// the return value of pthread_cond_signal, and then the errno.
pthread_cond_t local_cond;
struct iovec iov_remote_cond =
{ .iov_base = condSystemId, .iov_len = sizeof(cond_initializer) };
struct iovec iov_local_cond =
{ .iov_base = &local_cond, .iov_len = sizeof(cond_initializer) };
process_vm_readv(trace_pid, &iov_local_cond, 1, &iov_remote_cond, 1, 0);
if (memcmp(&local_cond, &cond_initializer, sizeof(cond_initializer)) != 0) {
mcprintf("\n*** ERROR (pthread_cond_wait/traceId: %d): The cond var\n"
"*** was never initialized.\n"
"*** Use pthread_cond_init() or PTHREAD_COND_INITIALIZER.\n"
"*** Additional McMini traces will not work with this bug.\n"
"*** McMini is exiting now.\n\n", traceId);
// No need to patch it with process_vm_writev. We will stop now.
mc_stop_model_checking(EXIT_FAILURE);
}
#endif
if (condThatExists -> shadow.state ==
MCConditionVariable::Shadow::undefined) {
condThatExists -> shadow.state = MCConditionVariable::Shadow::initialized;
}
}

assert(condThatExists -> shadow.state ==
MCConditionVariable::Shadow::initialized);
assert(condThatExists != nullptr);

MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
mutexThatExists != nullptr,
"Attempting to wait on a condition variable with an "
Expand All @@ -32,18 +113,6 @@ MCReadCondWait(const MCSharedTransition *shmTransition, void *shmData,
"Attempting to wait on a destroyed condition variable");

const auto threadThatRanId = shmTransition->executor;
const auto mutexAssociatedWithConditionVariable =
condThatExists->mutex;

if (mutexAssociatedWithConditionVariable != nullptr) {
MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
*mutexThatExists == *mutexAssociatedWithConditionVariable,
"A mutex has already been associated with this condition "
"variable. Attempting "
"to use another mutex with the same condition variable is "
"undefined");
}

auto threadThatRan = state->getThreadWithId(threadThatRanId);
return new MCCondWait(threadThatRan, condThatExists);
}
Expand Down