1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
5 * This program is free software; you can redistribute it and/or
6 * modify it under the terms of the GNU General Public License
7 * version 2 as published by the Free Software Foundation.
10 /** @file threads-model.h
11 * @brief Model Checker Thread class.
14 #ifndef __THREADS_MODEL_H__
15 #define __THREADS_MODEL_H__
21 #include "modeltypes.h"
22 #include "stl-model.h"
24 #include "classlist.h"
26 struct thread_params {
31 /** @brief Represents the state of a user Thread */
32 typedef enum thread_state {
33 /** Thread was just created and hasn't run yet */
35 /** Thread is running */
37 /** Thread is not currently running but is ready to run */
40 * Thread is waiting on another action (e.g., thread completion, lock
44 /** Thread has completed its execution */
49 /** @brief A Thread is created for each user-space thread */
52 Thread(thread_id_t tid);
53 Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent, EPRecord *r);
57 ucontext_t * get_context() {
61 thread_state get_state() const { return state; }
62 void set_state(thread_state s);
63 thread_id_t get_id() const;
64 thrd_t get_thrd_t() const { return *user_thread; }
65 Thread * get_parent() const { return parent; }
67 /** @return True if this thread is finished executing */
68 bool is_complete() const { return state == THREAD_COMPLETED; }
70 /** @return True if this thread is blocked */
71 bool is_blocked() const { return state == THREAD_BLOCKED; }
73 Thread * waiting_on();
74 void set_waiting(Thread *);
76 bool is_waiting_on(const Thread *t);
78 bool is_model_thread() const { return model_thread; }
80 friend void thread_startup();
83 * Intentionally NOT allocated with MODELALLOC or SNAPSHOTALLOC.
84 * Threads should be allocated on the user's normal (snapshotting) heap
85 * to allow their allocation/deallocation to follow the same pattern as
86 * the rest of the backtracked/replayed program.
88 void * operator new(size_t size) {
89 return Thread_malloc(size);
91 void operator delete(void *p, size_t size) {
94 void * operator new[](size_t size) {
95 return Thread_malloc(size);
97 void operator delete[](void *p, size_t size) {
100 EPRecord * getParentRecord() {return parentrecord;}
102 int create_context();
104 /** @brief The parent Thread which created this Thread */
105 Thread * const parent;
106 EPRecord * parentrecord;
107 void (*start_routine)(void *);
116 /** @brief Is this Thread a special model-checker thread? */
117 const bool model_thread;
120 Thread * thread_current();
122 static inline thread_id_t thrd_to_id(thrd_t t)
124 return t.priv->get_id();
128 * @brief Map a zero-based integer index to a unique thread ID
130 * This is the inverse of id_to_int
132 static inline thread_id_t int_to_id(int i)
138 * @brief Map a unique thread ID to a zero-based integer index
140 * This is the inverse of int_to_id
142 static inline int id_to_int(thread_id_t id)
147 #endif /* __THREADS_MODEL_H__ */