X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=threads-model.h;h=eb0fd438d388931ef0316231abd828d6e5295581;hb=bee1e27429b9a66e414eb83cf14e2089dd40a79e;hp=2cd09ab53739de7d327de3e5758af6b7ba66465d;hpb=ad52dcdb3a75a69242a392165934e942cb76513b;p=model-checker.git diff --git a/threads-model.h b/threads-model.h index 2cd09ab..eb0fd43 100644 --- a/threads-model.h +++ b/threads-model.h @@ -7,11 +7,11 @@ #include #include -#include #include "mymemory.h" #include #include "modeltypes.h" +#include "stl-model.h" struct thread_params { thrd_start_t func; @@ -104,6 +104,8 @@ public: * @see Thread::pending */ void set_pending(ModelAction *act) { pending = act; } + Thread * waiting_on() const; + /** * Remove one ModelAction from the waiting list * @return The ModelAction that was removed from the waiting list @@ -124,6 +126,18 @@ public: * to allow their allocation/deallocation to follow the same pattern as * the rest of the backtracked/replayed program. */ + void * operator new(size_t size) { + return Thread_malloc(size); + } + void operator delete(void *p, size_t size) { + Thread_free(p); + } + void * operator new[](size_t size) { + return Thread_malloc(size); + } + void operator delete[](void *p, size_t size) { + Thread_free(p); + } private: int create_context(); @@ -155,7 +169,7 @@ private: * list is used for thread joins, where another Thread waits for this * Thread to complete */ - std::vector< ModelAction *, SnapshotAlloc > wait_list; + SnapVector wait_list; /** * The value returned by the last action in this thread