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 The ModelAction to work on
  32          * @see MOEdgeWorkEntry
  33          */
  34         ModelAction *action;
  35 };
  36
  37 /**
  38  * @brief Work: perform initial promise, mo_graph checks on the current action
  39  *
  40  * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction
  41  * that is currently being explored. The current ModelAction (@a action) is the
  42  * only relevant parameter to this entry.
  43  */
  44 class CheckCurrWorkEntry : public WorkQueueEntry {
  45  public:
  46         /**
  47          * @brief Constructor for a "check current action" work entry
  48          * @param curr The current action
  49          */
  50         CheckCurrWorkEntry(ModelAction *curr) {
  51                 type = WORK_CHECK_CURR_ACTION;
  52                 action = curr;
  53         }
  54 };
  55
  56 /**
  57  * @brief Work: check a ModelAction for new mo_graph edges
  58  *
  59  * This WorkQueueEntry checks for new mo_graph edges for a particular
  60  * ModelAction (e.g., that was just generated or that updated its
  61  * synchronization). The ModelAction @a action is the only relevant parameter
  62  * to this entry.
  63  */
  64 class MOEdgeWorkEntry : public WorkQueueEntry {
  65  public:
  66         /**
  67          * @brief Constructor for a mo_edge work entry
  68          * @param updated The ModelAction which was updated, triggering this work
  69          */
  70         MOEdgeWorkEntry(ModelAction *updated) {
  71                 type = WORK_CHECK_MO_EDGES;
  72                 action = updated;
  73         }
  74 };
  75
  76 /** @brief typedef for the work queue type */
  77 typedef ModelList<WorkQueueEntry> work_queue_t;
  78
  79 #endif /* __WORKQUEUE_H__ */