mcexecution.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 #ifndef MCEXECUTION_H
  11 #define MCEXECUTION_H
  12 #include "hashtable.h"
  13 #include "execpoint.h"
  14 #include "stl-model.h"
  15 #include "classlist.h"
  16 #include <libinterface.h>
  17 #include "eprecord.h"
  18 #include "epvalue.h"
  19 #include "threads-model.h"
  20
  21 typedef HashTable<ExecPoint *, EPRecord *, uintptr_t, 0, model_malloc, model_calloc, model_free, ExecPointHash, ExecPointEquals> EPHashTable;
  22 typedef HashTable<const void *, MCID, uintptr_t, 4, snapshot_malloc, snapshot_calloc, snapshot_free> MemHashTable;
  23 typedef HashTable<EPValue *, EPValue *, uintptr_t, 0, model_malloc, model_calloc, model_free, EPValueHash, EPValueEquals> EPValueHashTable;
  24 typedef HashTable<const void *, RecordSet *, uintptr_t, 4, model_malloc, model_calloc, model_free> StoreLoadHashTable;
  25
  26
  27 struct RecordIntPair {
  28         EPRecord *record;
  29         unsigned int index;
  30 };
  31 inline unsigned int RP_hash_function(struct RecordIntPair * pair) {
  32         return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ pair->index;
  33 }
  34 inline bool RP_equals(struct RecordIntPair * key1, struct RecordIntPair * key2) {
  35         if (key1==NULL)
  36                 return key1==key2;
  37         return key1->record == key2->record && key1->index == key2->index;
  38 }
  39 typedef HashSet<struct RecordIntPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> EPRecordSet;
  40 typedef HSIterator<struct RecordIntPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> EPRecordIterator;
  41 typedef HashTable<EPRecord *, EPRecordSet *, uintptr_t, 4, model_malloc, model_calloc, model_free> EPRecordDepHashTable;
  42 typedef HashTable<struct RecordIntPair *, ModelVector<EPRecord *> *, uintptr_t, 4, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> RevDepHashTable;
  43
  44 struct MCExecution_snapshot {
  45         MCExecution_snapshot();
  46         ~MCExecution_snapshot();
  47         unsigned int next_thread_id;
  48
  49         SNAPSHOTALLOC;
  50 };
  51
  52 class MCExecution {
  53 public:
  54         MCExecution();
  55         ~MCExecution();
  56         EPRecord * getOrCreateCurrRecord(EventType et, bool * isNew, uintptr_t offset, unsigned int numinputs, uint len, bool br_anyvalue);
  57         MCID getNextMCID() { return ++currid; }
  58         MCID loadMCID(MCID maddr, uintptr_t offset);
  59         void storeMCID(MCID maddr, uintptr_t offset, MCID val);
  60         MCID nextRMW(MCID addr, uintptr_t offset, MCID oldval, MCID valarg);
  61         void store(void *addr, uint64_t val, int len);
  62         uint64_t load(const void *addr, int len);
  63         uint64_t rmw(enum atomicop op, void *addr, uint size, uint64_t currval, uint64_t oldval, uint64_t valarg);
  64         void reset();
  65         MCID branchDir(MCID dir, int direction, int numdirs, bool anyvalue);
  66         void merge(MCID mcid);
  67         MCID function(uint functionidentifier, int numbytesretval, uint64_t val, uint num_args, MCID *mcids);
  68         uint64_t equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval);
  69         MCID phi(MCID input);
  70         MCID loop_phi(MCID input);
  71         void * alloc(size_t bytes);
  72 #ifdef TSO
  73         void fence();
  74         void doStore(EPValue *epval);
  75         void doStore(thread_id_t tid);
  76         bool isEmptyStoreBuffer(thread_id_t tid);
  77         EPValue *getStoreBuffer(thread_id_t tid) {int thread=id_to_int(tid); if ((*storebuffer)[thread]->empty()) return NULL; else return (*storebuffer)[id_to_int(tid)]->front();}
  78 #endif
  79         void enterLoop();
  80         void exitLoop();
  81         void loopIterate();
  82         void threadCreate(thrd_t *t, thrd_start_t start, void *arg);
  83         void threadJoin(Thread *th);
  84         void threadYield();
  85         void threadFinish();
  86         MCScheduler * get_scheduler() const { return scheduler; }
  87         Planner * get_planner() const { return planner; }
  88         EPValue * getEPValue(EPRecord * record, bool * isNew, const void *addr, uint64_t val, int len);
  89         void recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids);
  90         void add_thread(Thread *t);
  91         thread_id_t get_next_tid();
  92         unsigned int get_num_threads() {return snap_fields->next_thread_id;};
  93         void set_current_thread(Thread *t);
  94         Thread * get_current_thread() {return curr_thread;}
  95         ExecPoint * get_execpoint(thread_id_t tid) {return (*ExecPointList)[id_to_int(tid)];}
  96         Thread * get_thread(thread_id_t tid) {return (*ThreadList)[id_to_int(tid)];}
  97         void addStoreTable(const void *addr, EPRecord *record);
  98         void addLoadTable(const void *addr, EPRecord *record);
  99         RecordSet * getStoreTable(const void *addr);
 100         RecordSet * getLoadTable(const void *addr);
 101         void recordRMWChange(EPRecord *load, const void *addr, uint64_t valarg, uint64_t oldval, uint64_t newval);
 102         void recordFunctionChange(EPRecord *function, uint64_t val);
 103         void recordLoadChange(EPRecord *function, const void *addr);
 104         void recordStoreChange(EPRecord *function, const void *addr, uint64_t val);
 105         EPRecord * getEPRecord(MCID id);
 106         EPValue * getEPValue(MCID id);
 107         void addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index);
 108         EPRecordSet *getDependences(EPRecord *record) {return eprecorddep->get(record);}
 109         ModelVector<EPRecord *> * getRevDependences(EPRecord *record, uint index);
 110         void threadStart(EPRecord *parent);
 111
 112         bool compatibleStoreLoad(EPRecord *store, EPRecord *load) {
 113                 return store!=load;
 114         }
 115         ModelVector<EPRecord *> * getAlwaysExecuted() {return alwaysexecuted;}
 116         ModelVector<EPRecord *> * getJoins() {return joinvec;}
 117         void evalGoal(EPRecord *record, CGoal *goal);
 118         void dumpExecution();
 119         EPRecord * getRecord(ExecPoint * ep) {return EPTable->get(ep);}
 120
 121         MEMALLOC;
 122 private:
 123         EPHashTable * EPTable;
 124         EPValueHashTable * EPValueTable;
 125         MemHashTable *memtable;
 126         StoreLoadHashTable *storetable;
 127         StoreLoadHashTable *loadtable;
 128         SnapVector<EPValue *> *EPList;
 129         SnapVector<Thread *> *ThreadList;
 130 #ifdef TSO
 131         SnapVector<SnapList<EPValue *> *> *storebuffer;
 132 #endif
 133         SnapVector<ExecPoint *> *ExecPointList;
 134         SnapVector<EPValue *> *CurrBranchList;
 135         ExecPoint * currexecpoint;
 136         MCScheduler * scheduler;
 137         Planner * planner;
 138         struct MCExecution_snapshot * const snap_fields;
 139         Thread * curr_thread;
 140         EPValue *currbranch;
 141         EPRecordDepHashTable *eprecorddep;
 142         RevDepHashTable *revrecorddep;
 143         ModelVector<EPRecord *> * alwaysexecuted;
 144         ModelVector<EPRecord *> * lastloopexit;
 145         ModelVector<EPRecord *> * joinvec;
 146         ModelVector<CGoalSet *> * sharedgoals;
 147         ModelVector<RecordSet *> * sharedfuncrecords;
 148
 149         MCID currid;
 150         MCID id_addr;
 151         MCID id_oldvalue;
 152         MCID id_value;
 153         MCID id_retval;
 154         uintptr_t id_addr_offset;
 155         uint schedule_graph;
 156 };
 157
 158 #endif