Skip to content
Open
Show file tree
Hide file tree
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
43 changes: 27 additions & 16 deletions include/mcmini/coordinator/model_to_system_map.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,11 @@
* the coordinator to handle aliasing etc. by using the trace as a total
* ordering on object-creation events. Until we run into this issue, we leave it
* for future development.
*
* @note this correspondence covers visible _objects_ only. Runners (threads)
* are identified by the `runner_id_t` that `libmcmini.so` assigns them, not by
* the address of their `pthread_t` descriptor, which glibc recycles. See
* `observe_runner()`.
*/
class model_to_system_map final {
private:
Expand All @@ -43,14 +48,9 @@ class model_to_system_map final {

model::state::objid_t get_model_of_object(
real_world::remote_address<void>) const;
model::state::runner_id_t get_model_of_runner(
real_world::remote_address<void>) const;
bool contains(real_world::remote_address<void> addr) const {
return get_model_of_object(addr) != model::invalid_objid;
}
bool contains_runner(real_world::remote_address<void> addr) const {
return get_model_of_runner(addr) != model::invalid_rid;
}

using runner_generation_function =
std::function<const model::transition *(model::state::runner_id_t)>;
Expand All @@ -66,16 +66,27 @@ class model_to_system_map final {
model::state::objid_t observe_object(real_world::remote_address<void>,
const model::visible_object_state *);

// TODO: Does it make sense to be able to add a runner without a transition
// and then later (retroactively) give it a transition (in _this_ interface
// that is)
model::state::runner_id_t observe_runner(real_world::remote_address<void>,
const model::runner_state *);
/**
* @brief Record the presence of a new runner (thread) which `libmcmini.so`
* has assigned the id `id` in the target process.
*
* Unlike visible objects, runners are _not_ identified by a remote address.
* A `pthread_t` is the address of a thread descriptor which glibc recycles
* once a thread is joined, so the same address routinely denotes different
* threads over the lifetime of the target. Instead, `libmcmini.so` assigns
* each thread a `runner_id_t` from a monotonic counter and reports that id
* directly; the same id also indexes the thread's mailbox in shared memory.
*
* The model allocates runner ids the same way (in order of discovery), so
* the id the model assigns must agree with the one the target reports.
*
* @throws std::runtime_error if the model assigns an id other than `id`,
* which means the model and the target have disagreed about the set of
* live threads.
*/
void observe_runner(model::state::runner_id_t id,
const model::runner_state *);
void observe_runner(model::state::runner_id_t id, const model::runner_state *,
runner_generation_function f);
void observe_runner_transition(const model::transition *);
model::state::runner_id_t observe_runner(real_world::remote_address<void>,
const model::runner_state *,
const model::transition *);
model::state::runner_id_t observe_runner(real_world::remote_address<void>,
const model::runner_state *,
runner_generation_function f);
};
4 changes: 3 additions & 1 deletion src/examples/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,10 @@ add_executable(cv-test cv-test.c)
add_executable(deadly-embrace deadly-embrace.c)
add_executable(fifo-example fifo.cpp)
add_executable(producer-consumer producer-consumer.c)
target_link_libraries(hello-world PUBLIC -pthread)
add_executable(recycled-thread recycled-thread.c)
target_link_libraries(hello-world PUBLIC -pthread libmcmini)
target_link_libraries(cv-hello-world PUBLIC -pthread)
target_link_libraries(cv-test PUBLIC -pthread)
target_link_libraries(deadly-embrace PUBLIC -pthread)
target_link_libraries(producer-consumer PUBLIC -pthread)
target_link_libraries(recycled-thread PUBLIC -pthread libmcmini)
28 changes: 28 additions & 0 deletions src/examples/recycled-thread.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
// Creates and joins workers one at a time. glibc caches the joined thread's
// stack, so every round hands back the same `pthread_t`. McMini must identify
// each worker by the id `libmcmini.so` assigned it, not by that descriptor.

#include <pthread.h>
#include <stdio.h>

#define ROUNDS 3

static pthread_mutex_t mutex;

static void *worker(void *unused) {
pthread_mutex_lock(&mutex);
pthread_mutex_unlock(&mutex);
return NULL;
}

int main(int argc, char *argv[]) {
pthread_mutex_init(&mutex, NULL);

for (int i = 0; i < ROUNDS; i++) {
pthread_t worker_thread;
pthread_create(&worker_thread, NULL, &worker, NULL);
printf("round %d: pthread_t = %p\n", i, (void *)worker_thread);
pthread_join(worker_thread, NULL);
}
return 0;
}
38 changes: 31 additions & 7 deletions src/lib/wrappers.c
Original file line number Diff line number Diff line change
Expand Up @@ -34,17 +34,21 @@ void insert_pthread_map(pthread_t t, runner_id_t v) {
pthread_rwlock_unlock(&pthread_map_lock);
}

// NOTE: `insert_pthread_map()` prepends, so the first match is the most
// recently created thread holding this descriptor. That is the only thread a
// caller may legally join: glibc recycles a `pthread_t` once its thread has
// been joined, at which point POSIX says the old handle is no longer valid.
runner_id_t search_pthread_map(pthread_t t) {
pthread_rwlock_rdlock(&pthread_map_lock);
pthread_map_t *cur = head;
while (cur) {
runner_id_t value = RID_INVALID;
pthread_rwlock_rdlock(&pthread_map_lock);
for (pthread_map_t *cur = head; cur != NULL; cur = cur->next) {
if (pthread_equal(cur->thread, t)) {
return cur->value;
value = cur->value;
break;
}
cur = cur->next;
}
pthread_rwlock_unlock(&pthread_map_lock);
return RID_INVALID;
return value;
}


Expand Down Expand Up @@ -453,12 +457,18 @@ MCMINI_NO_RETURN void mc_transparent_abort(void) {
struct mc_thread_routine_arg {
void *arg;
thread_routine routine;

// The id `libmcmini.so` assigned the child. The child publishes it here
// before posting `mc_pthread_create_binary_sem`, so it is readable by the
// creator as soon as `sem_wait()` returns.
runner_id_t child_rid;
sem_t mc_pthread_create_binary_sem;
};

void *mc_thread_routine_wrapper(void *arg) {
runner_id_t rid = mc_register_this_thread();
struct mc_thread_routine_arg *unwrapped_arg = arg;
unwrapped_arg->child_rid = rid;
switch (get_current_mode()) {
case PRE_DMTCP_INIT:
case PRE_CHECKPOINT_THREAD:
Expand Down Expand Up @@ -619,6 +629,7 @@ int mc_pthread_create(pthread_t *thread, const pthread_attr_t *attr,
malloc(sizeof(struct mc_thread_routine_arg));
wrapped_arg->arg = arg;
wrapped_arg->routine = routine;
wrapped_arg->child_rid = RID_INVALID;
libpthread_sem_init(&wrapped_arg->mc_pthread_create_binary_sem, 0, 0);
int rc = libdmtcp_pthread_create(
thread, attr, &dmtcp_create_checkpoint_thread_wrapper, wrapped_arg);
Expand All @@ -645,6 +656,7 @@ int mc_pthread_create(pthread_t *thread, const pthread_attr_t *attr,
malloc(sizeof(struct mc_thread_routine_arg));
libmcmini_controlled_thread_arg->arg = arg;
libmcmini_controlled_thread_arg->routine = routine;
libmcmini_controlled_thread_arg->child_rid = RID_INVALID;
// TODO: Handle the errors that can occur when
// pthread_create is called. They are unlikely to
// occur in practice, but should be handled
Expand All @@ -669,6 +681,7 @@ int mc_pthread_create(pthread_t *thread, const pthread_attr_t *attr,
malloc(sizeof(struct mc_thread_routine_arg));
libmcmini_controlled_thread_arg->arg = arg;
libmcmini_controlled_thread_arg->routine = routine;
libmcmini_controlled_thread_arg->child_rid = RID_INVALID;
libpthread_sem_init(
&libmcmini_controlled_thread_arg->mc_pthread_create_binary_sem, 0,
0);
Expand All @@ -690,7 +703,18 @@ int mc_pthread_create(pthread_t *thread, const pthread_attr_t *attr,
libpthread_sem_wait(
&libmcmini_controlled_thread_arg->mc_pthread_create_binary_sem);

memcpy_v(thread_get_mailbox()->cnts, thread, sizeof(pthread_t));
// Safe to read: the child is parked in
// `thread_await_scheduler()` and cannot reach the `free()` at the end of
// `mc_thread_routine_wrapper()` until the scheduler runs it, which it
// will not do before processing the THREAD_CREATE we are about to send.
const runner_id_t child_rid = libmcmini_controlled_thread_arg->child_rid;
assert(child_rid != RID_INVALID);

// Report the id `libmcmini.so` assigned the child rather than its
// `pthread_t`: glibc recycles thread descriptors, so the same
// `pthread_t` denotes different threads over the run and would make the
// model bind a new thread to a dead thread's runner.
memcpy_v(thread_get_mailbox()->cnts, &child_rid, sizeof(runner_id_t));
thread_get_mailbox()->type = THREAD_CREATE_TYPE;
thread_wake_scheduler_and_wait();
return rv;
Expand Down
75 changes: 26 additions & 49 deletions src/mcmini/coordinator/coordinator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -102,17 +102,6 @@ void coordinator::return_to_depth(uint32_t n) {
<< "\n\n**************** AFTER RESTORATION *********************";
}

model::state::runner_id_t model_to_system_map::get_model_of_runner(
remote_address<void> handle) const {
model::state::objid_t objid = get_model_of_object(handle);
if (objid != model::invalid_objid) {
return _coordinator.get_current_program_model()
.get_state_sequence()
.get_runner_id_for_obj(objid);
}
return model::invalid_rid;
}

model::state::objid_t model_to_system_map::get_model_of_object(
remote_address<void> handle) const {
if (_coordinator.system_address_mapping.count(handle) > 0) {
Expand All @@ -136,50 +125,38 @@ model::state::objid_t model_to_system_map::observe_object(
return new_objid;
}

model::state::runner_id_t model_to_system_map::observe_runner(
real_world::remote_address<void> rp_vobj_handle,
const model::runner_state *vobs, const model::transition *t) {
return observe_runner(std::move(rp_vobj_handle), vobs,
[t](runner_id_t id) { return t; });
namespace {

void assert_runner_ids_agree(model::state::runner_id_t reported_by_target,
model::state::runner_id_t assigned_by_model) {
if (reported_by_target == assigned_by_model) return;
std::stringstream ss;
ss << "The target reported a new thread with id " << reported_by_target
<< ", but the model assigned it the id " << assigned_by_model
<< ". The model and the target disagree about which threads are live; "
"the id also indexes the thread's mailbox, so the coordinator can no "
"longer address the threads it is scheduling.";
throw std::runtime_error(ss.str());
}

model::state::runner_id_t model_to_system_map::observe_runner(
real_world::remote_address<void> rp_vobj_handle,
const model::runner_state *vobs, runner_generation_function f) {
if (contains(rp_vobj_handle)) {
throw std::runtime_error(
"Attempting to rebind a remote address to an object that already "
"exists in the model. Did you check that the object doesn't already "
"exist?");
}
model::state::runner_id_t const new_runner_id =
_coordinator.current_program_model.discover_runner(vobs, std::move(f));
model::state::objid_t const new_objid =
_coordinator.get_current_program_model()
.get_state_sequence()
.get_objid_for_runner(new_runner_id);
_coordinator.system_address_mapping.insert({rp_vobj_handle, new_objid});
return new_runner_id;
} // namespace

void model_to_system_map::observe_runner(model::state::runner_id_t id,
const model::runner_state *vobs,
runner_generation_function f) {
assert_runner_ids_agree(
id, _coordinator.current_program_model.discover_runner(vobs, std::move(f)));
}

void model_to_system_map::observe_runner(model::state::runner_id_t id,
const model::runner_state *rs) {
assert_runner_ids_agree(
id,
_coordinator.current_program_model.get_current_state().add_runner(rs));
}

void model_to_system_map::observe_runner_transition(
const model::transition *t) {
_coordinator.current_program_model.get_pending_transitions().set_transition(
t);
}

model::state::runner_id_t model_to_system_map::observe_runner(
real_world::remote_address<void> rp_vobj_handle,
const model::runner_state *rs) {
// TODO: Remove code duplication here. Also there's a better way to do all of
// this I think (instead of e.g. needing to add similar methods onto
// `model::program`)
model::state::runner_id_t const new_runner_id =
_coordinator.current_program_model.get_current_state().add_runner(rs);
model::state::objid_t const new_objid =
_coordinator.get_current_program_model()
.get_state_sequence()
.get_objid_for_runner(new_runner_id);
_coordinator.system_address_mapping.insert({rp_vobj_handle, new_objid});
return new_runner_id;
}
7 changes: 3 additions & 4 deletions src/mcmini/mcmini.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -250,10 +250,9 @@ void do_model_checking_from_dmtcp_ckpt_file(const config& config) {
return lhs.thrd_state.id < rhs.thrd_state.id;
});

for (const ::visible_object& recorded_thread : recorded_threads) {
recorder.observe_runner(
(void*)recorded_thread.thrd_state.pthread_desc,
translate_recorded_runner_to_model(recorded_thread));
for (const ::visible_object &recorded_thread : recorded_threads) {
recorder.observe_runner(recorded_thread.thrd_state.id,
translate_recorded_runner_to_model(recorded_thread));
}

for (const ::visible_object& recorded_thread : recorded_threads) {
Expand Down
14 changes: 6 additions & 8 deletions src/mcmini/model/transitions/thread.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,12 @@ using namespace objects;
transition* thread_create_callback(runner_id_t p,
const volatile runner_mailbox& rmb,
model_to_system_map& m) {
pthread_t new_thread;
memcpy_v(&new_thread, static_cast<const volatile void*>(&rmb.cnts),
sizeof(pthread_t));
if (!m.contains_runner((void*)new_thread))
m.observe_runner(
(void*)new_thread, new thread(thread::embryo),
[](runner_id_t id) { return new transitions::thread_start(id); });
const runner_id_t new_thread_id = m.get_model_of_runner((void*)new_thread);
runner_id_t new_thread_id;
memcpy_v(&new_thread_id, static_cast<const volatile void*>(&rmb.cnts),
sizeof(runner_id_t));
m.observe_runner(
new_thread_id, new thread(thread::embryo),
[](runner_id_t id) { return new transitions::thread_start(id); });
return new transitions::thread_create(p, new_thread_id);
}

Expand Down