README.md: add End of Execution Summary section
[model-checker.git] / 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__ */