Include dependency graph for weak_memory.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Macros | |
| #define | OPT_WMM_MEMORY_MODEL "(mm):" |
| #define | OPT_WMM_INSTRUMENTATION_STRATEGIES |
| #define | OPT_WMM_LIMITS |
| #define | OPT_WMM_LOOPS |
| #define | OPT_WMM_MISC |
| #define | OPT_WMM |
| #define | HELP_WMM_FULL |
Functions | |
| 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) |
| void | introduce_temporaries (value_setst &, symbol_tablet &, const irep_idt &function, goto_programt &, messaget &message) |
| all access to shared variables is pushed into assignments More... | |
Detailed Description
Weak Memory Instrumentation for Threaded Goto Programs
Definition in file weak_memory.h.
Macro Definition Documentation
◆ HELP_WMM_FULL
| #define HELP_WMM_FULL |
Value:
" --mm <tso,pso,rmo,power> instruments a weak memory model\n" \
" --scc detects critical cycles per SCC (one thread per SCC)\n" /* NOLINT(whitespace/line_length) */ \
" --one-event-per-cycle only instruments one event per cycle\n" \
" --minimum-interference instruments an optimal number of events\n" \
" --my-events only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \
" --read-first|--write-first only instrument cycles where a read or \n" \
" write occurs as first event, respectively\n" \
" --max-var N limit cycles to N variables read/written\n" \
" --max-po-trans N limit cycles to N program-order edges\n" \
" --ignore-arrays instrument arrays as a single object\n" \
" --cav11 always instrument shared variables, even\n" \
" when they are not part of any cycle\n" \
" --force-loop-duplication|--no-loop-duplication\n" \
" optional program transformation to\n" \
" construct cycles in program loops\n" \
" --cfg-kill enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \
" --no-dependencies no dependency analysis\n" \
" --no-po-rendering no representation of the threads in the dot\n"\
" --hide-internals do not include thread-internal (Rfi)\n" \
" events in dot output\n" \
" --render-cluster-file clusterises the dot by files\n" \
" --render-cluster-function clusterises the dot by functions\n"
Definition at line 94 of file weak_memory.h.
◆ OPT_WMM
| #define OPT_WMM |
Value:
OPT_WMM_MEMORY_MODEL \
OPT_WMM_INSTRUMENTATION_STRATEGIES \
OPT_WMM_LIMITS \
OPT_WMM_LOOPS \
OPT_WMM_MISC \
Definition at line 86 of file weak_memory.h.
◆ OPT_WMM_INSTRUMENTATION_STRATEGIES
| #define OPT_WMM_INSTRUMENTATION_STRATEGIES |
Value:
"(one-event-per-cycle)" \
"(minimum-interference)" \
"(read-first)" \
"(write-first)" \
"(my-events)" \
Definition at line 60 of file weak_memory.h.
◆ OPT_WMM_LIMITS
| #define OPT_WMM_LIMITS |
Value:
"(max-var):" \
"(max-po-trans):" \
Definition at line 67 of file weak_memory.h.
◆ OPT_WMM_LOOPS
| #define OPT_WMM_LOOPS |
Value:
"(force-loop-duplication)" \
"(no-loop-duplication)" \
Definition at line 71 of file weak_memory.h.
◆ OPT_WMM_MEMORY_MODEL
| #define OPT_WMM_MEMORY_MODEL "(mm):" |
Definition at line 58 of file weak_memory.h.
◆ OPT_WMM_MISC
| #define OPT_WMM_MISC |
Value:
"(scc)" \
"(cfg-kill)" \
"(no-dependencies)" \
"(no-po-rendering)" \
"(render-cluster-file)" \
"(render-cluster-function)" \
"(cav11)" \
"(hide-internals)" \
"(ignore-arrays)" \
Definition at line 75 of file weak_memory.h.
Function Documentation
◆ introduce_temporaries()
| 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 at line 38 of file weak_memory.cpp.
◆ weak_memory()
| 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 | ||
| ) |
Definition at line 107 of file weak_memory.cpp.
