cprover
weak_memory.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Weak Memory Instrumentation for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: September 2011
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
16 
17 #include "wmm.h"
18 
19 #include <util/irep.h>
20 
21 class symbol_tablet;
22 class value_setst;
23 class goto_modelt;
24 class message_handlert;
25 class goto_programt;
26 class messaget;
27 
28 void weak_memory(
29  memory_modelt model,
30  value_setst &,
31  goto_modelt &,
32  bool SCC,
33  instrumentation_strategyt event_stategy,
34  bool no_cfg_kill,
35  bool no_dependencies,
36  loop_strategyt duplicate_body,
37  unsigned max_var,
38  unsigned max_po_trans,
39  bool render_po,
40  bool render_file,
41  bool render_function,
42  bool cav11_option,
43  bool hide_internals,
45  bool ignore_arrays);
46 
48  value_setst &,
49  symbol_tablet &,
50  const irep_idt &function,
51  goto_programt &,
52 #ifdef LOCAL_MAY
53  const goto_functionst::goto_functiont &goto_function,
54 #endif
55  messaget &message);
56 
57 // clang-format off
58 #define OPT_WMM_MEMORY_MODEL "(mm):"
59 
60 #define OPT_WMM_INSTRUMENTATION_STRATEGIES \
61  "(one-event-per-cycle)" \
62  "(minimum-interference)" \
63  "(read-first)" \
64  "(write-first)" \
65  "(my-events)" \
66 
67 #define OPT_WMM_LIMITS \
68  "(max-var):" \
69  "(max-po-trans):" \
70 
71 #define OPT_WMM_LOOPS \
72  "(force-loop-duplication)" \
73  "(no-loop-duplication)" \
74 
75 #define OPT_WMM_MISC \
76  "(scc)" \
77  "(cfg-kill)" \
78  "(no-dependencies)" \
79  "(no-po-rendering)" \
80  "(render-cluster-file)" \
81  "(render-cluster-function)" \
82  "(cav11)" \
83  "(hide-internals)" \
84  "(ignore-arrays)" \
85 
86 #define OPT_WMM \
87  OPT_WMM_MEMORY_MODEL \
88  OPT_WMM_INSTRUMENTATION_STRATEGIES \
89  OPT_WMM_LIMITS \
90  OPT_WMM_LOOPS \
91  OPT_WMM_MISC \
92 
93 
94 #define HELP_WMM_FULL \
95  " --mm <tso,pso,rmo,power> instruments a weak memory model\n" \
96  " --scc detects critical cycles per SCC (one thread per SCC)\n" /* NOLINT(whitespace/line_length) */ \
97  " --one-event-per-cycle only instruments one event per cycle\n" \
98  " --minimum-interference instruments an optimal number of events\n" \
99  " --my-events only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \
100  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \
101  " --no-dependencies no dependency analysis\n" \
102  " --no-po-rendering no representation of the threads in the dot\n"\
103  " --render-cluster-file clusterises the dot by files\n" \
104  " --render-cluster-function clusterises the dot by functions\n"
105 
106 // clang-format on
107 
108 #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
The symbol table.
Definition: symbol_table.h:14
void introduce_temporaries(value_setst &, symbol_tablet &, const irep_idt &function, goto_programt &, messaget &message)
all access to shared variables is pushed into assignments
Definition: weak_memory.cpp:38
void weak_memory(memory_modelt model, value_setst &, goto_modelt &, bool SCC, instrumentation_strategyt event_stategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned max_var, unsigned max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &, bool ignore_arrays)
memory models
memory_modelt
Definition: wmm.h:18
loop_strategyt
Definition: wmm.h:37
instrumentation_strategyt
Definition: wmm.h:27