threads-model.h

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   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.
   8  */
   9
  10 /** @file threads-model.h
  11  *  @brief Model Checker Thread class.
  12  */
  13
  14 #ifndef __THREADS_MODEL_H__
  15 #define __THREADS_MODEL_H__
  16
  17 #include <stdint.h>
  18
  19 #include "mymemory.h"
  20 #include <threads.h>
  21 #include "modeltypes.h"
  22 #include "stl-model.h"
  23 #include "context.h"
  24 #include "classlist.h"
  25
  26 struct thread_params {
  27         thrd_start_t func;
  28         void *arg;
  29 };
  30
  31 /** @brief Represents the state of a user Thread */
  32 typedef enum thread_state {
  33         /** Thread was just created and hasn't run yet */
  34         THREAD_CREATED,
  35         /** Thread is running */
  36         THREAD_RUNNING,
  37         /** Thread is not currently running but is ready to run */
  38         THREAD_READY,
  39         /**
  40          * Thread is waiting on another action (e.g., thread completion, lock
  41          * release, etc.)
  42          */
  43         THREAD_BLOCKED,
  44         /** Thread has completed its execution */
  45         THREAD_COMPLETED
  46 } thread_state;
  47
  48
  49 /** @brief A Thread is created for each user-space thread */
  50 class Thread {
  51  public:
  52         Thread(thread_id_t tid);
  53         Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent, EPRecord *r);
  54         ~Thread();
  55         void complete();
  56
  57         ucontext_t * get_context() {
  58                 return &context;
  59         }
  60
  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; }
  66
  67         /** @return True if this thread is finished executing */
  68         bool is_complete() const { return state == THREAD_COMPLETED; }
  69
  70         /** @return True if this thread is blocked */
  71         bool is_blocked() const { return state == THREAD_BLOCKED; }
  72
  73         Thread * waiting_on();
  74         void set_waiting(Thread *);
  75
  76         bool is_waiting_on(const Thread *t);
  77
  78         bool is_model_thread() const { return model_thread; }
  79
  80         friend void thread_startup();
  81
  82         /**
  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.
  87          */
  88         void * operator new(size_t size) {
  89                 return Thread_malloc(size);
  90         }
  91         void operator delete(void *p, size_t size) {
  92                 Thread_free(p);
  93         }
  94         void * operator new[](size_t size) {
  95                 return Thread_malloc(size);
  96         }
  97         void operator delete[](void *p, size_t size) {
  98                 Thread_free(p);
  99         }
 100         EPRecord * getParentRecord() {return parentrecord;}
 101  private:
 102         int create_context();
 103
 104         /** @brief The parent Thread which created this Thread */
 105         Thread * const parent;
 106         EPRecord * parentrecord;
 107         void (*start_routine)(void *);
 108         void *arg;
 109         ucontext_t context;
 110         void *stack;
 111         thrd_t *user_thread;
 112         Thread *waiting;
 113         thread_id_t id;
 114         thread_state state;
 115
 116         /** @brief Is this Thread a special model-checker thread? */
 117         const bool model_thread;
 118 };
 119
 120 Thread * thread_current();
 121
 122 static inline thread_id_t thrd_to_id(thrd_t t)
 123 {
 124         return t.priv->get_id();
 125 }
 126
 127 /**
 128  * @brief Map a zero-based integer index to a unique thread ID
 129  *
 130  * This is the inverse of id_to_int
 131  */
 132 static inline thread_id_t int_to_id(int i)
 133 {
 134         return i;
 135 }
 136
 137 /**
 138  * @brief Map a unique thread ID to a zero-based integer index
 139  *
 140  * This is the inverse of int_to_id
 141  */
 142 static inline int id_to_int(thread_id_t id)
 143 {
 144         return id;
 145 }
 146
 147 #endif /* __THREADS_MODEL_H__ */