workqueue.h

   1 /**
   2  * @file workqueue.h
   3  * @brief Provides structures for queueing ModelChecker actions to be taken
   4  */
   5
   6 #ifndef __WORKQUEUE_H__
   7 #define __WORKQUEUE_H__
   8
   9 #include "mymemory.h"
  10 #include "stl-model.h"
  11
  12 class ModelAction;
  13
  14 typedef enum {
  15         WORK_NONE = 0,           /**< No work to be done */
  16         WORK_CHECK_CURR_ACTION,  /**< Check the current action; used for the
  17                                       first action of the work loop */
  18         WORK_CHECK_RELEASE_SEQ,  /**< Check if any pending release sequences
  19                                       are resolved */
  20         WORK_CHECK_MO_EDGES,     /**< Check if new mo_graph edges can be added */
  21 } model_work_t;
  22
  23 /**
  24  */
  25 class WorkQueueEntry {
  26  public:
  27         /** @brief Type of work queue entry */
  28         model_work_t type;
  29
  30         /**
  31          * @brief Object affected
  32          * @see CheckRelSeqWorkEntry
  33          */
  34         void *location;
  35
  36         /**
  37          * @brief The ModelAction to work on
  38          * @see MOEdgeWorkEntry
  39          */
  40         ModelAction *action;
  41 };
  42
  43 /**
  44  * @brief Work: perform initial promise, mo_graph checks on the current action
  45  *
  46  * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction
  47  * that is currently being explored. The current ModelAction (@a action) is the
  48  * only relevant parameter to this entry.
  49  */
  50 class CheckCurrWorkEntry : public WorkQueueEntry {
  51  public:
  52         /**
  53          * @brief Constructor for a "check current action" work entry
  54          * @param curr The current action
  55          */
  56         CheckCurrWorkEntry(ModelAction *curr) {
  57                 type = WORK_CHECK_CURR_ACTION;
  58                 location = NULL;
  59                 action = curr;
  60         }
  61 };
  62
  63 /**
  64  * @brief Work: check an object location for resolved release sequences
  65  *
  66  * This WorkQueueEntry checks synchronization and the mo_graph for resolution
  67  * of any release sequences. The object @a location is the only relevant
  68  * parameter to this entry.
  69  */
  70 class CheckRelSeqWorkEntry : public WorkQueueEntry {
  71  public:
  72         /**
  73          * @brief Constructor for a "check release sequences" work entry
  74          * @param l The location which must be checked for release sequences
  75          */
  76         CheckRelSeqWorkEntry(void *l) {
  77                 type = WORK_CHECK_RELEASE_SEQ;
  78                 location = l;
  79                 action = NULL;
  80         }
  81 };
  82
  83 /**
  84  * @brief Work: check a ModelAction for new mo_graph edges
  85  *
  86  * This WorkQueueEntry checks for new mo_graph edges for a particular
  87  * ModelAction (e.g., that was just generated or that updated its
  88  * synchronization). The ModelAction @a action is the only relevant parameter
  89  * to this entry.
  90  */
  91 class MOEdgeWorkEntry : public WorkQueueEntry {
  92  public:
  93         /**
  94          * @brief Constructor for a mo_edge work entry
  95          * @param updated The ModelAction which was updated, triggering this work
  96          */
  97         MOEdgeWorkEntry(ModelAction *updated) {
  98                 type = WORK_CHECK_MO_EDGES;
  99                 location = NULL;
 100                 action = updated;
 101         }
 102 };
 103
 104 /** @brief typedef for the work queue type */
 105 typedef ModelList<WorkQueueEntry> work_queue_t;
 106
 107 #endif /* __WORKQUEUE_H__ */