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