cprover
Loading...
Searching...
No Matches
weak_memory.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Weak Memory Instrumentation for Threaded Goto Programs
4
5Author: Daniel Kroening
6
7Date: 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
21class symbol_tablet;
22class value_setst;
23class goto_modelt;
25class goto_programt;
26class messaget;
27
28void weak_memory(
29 memory_modelt model,
32 bool SCC,
34 bool no_cfg_kill,
35 bool no_dependencies,
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
50 const irep_idt &function,
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
The symbol table.
void introduce_temporaries(value_setst &, symbol_tablet &, const irep_idt &function, goto_programt &, messaget &message)
all access to shared variables is pushed into assignments
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