Loading...
Searching...
No Matches
Weak Memory Instrumentation for Threaded Goto Programs. More...
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 | |
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:
" {y--mm} [{ytso}|{ypso}|{yrmo}|{ypower}] \t " \
"instruments a weak memory model\n" \
" {y--scc} \t detects critical cycles per SCC (one thread per SCC)\n" \
" {y--one-event-per-cycle} \t only instruments one event per cycle\n" \
" {y--minimum-interference} \t instruments an optimal number of events\n" \
" {y--my-events} \t only instruments events whose ids appear in inst.evt\n" \
" {y--read-first}, {y--write-first} \t " \
"only instrument cycles where a read or write occurs as first event, " \
"respectively\n" \
" {y--max-var} {uN} \t limit cycles to {uN} variables read/written\n" \
" {y--max-po-trans} {uN} \t limit cycles to {uN} program-order edges\n" \
" {y--ignore-arrays} \t instrument arrays as a single object\n" \
" {y--cav11} \t " \
"always instrument shared variables, even when they are not part of " \
"any cycle\n" \
" {y--force-loop-duplication}, {y--no-loop-duplication} \t " \
"optional program transformation to construct cycles in program loops\n" \
" {y--cfg-kill} \t enables symbolic execution used to reduce spurious " \
"cycles\n" \
" {y--no-dependencies} \t no dependency analysis\n" \
" {y--no-po-rendering} \t no representation of the threads in the dot\n" \
" {y--hide-internals} \t do not include thread-internal (Rfi) events in " \
"dot output\n" \
" {y--render-cluster-file} \t clusterises the dot by files\n" \
" {y--render-cluster-function} \t clusterises the dot by functions\n"
Definition at line 92 of file weak_memory.h.
◆ OPT_WMM
| #define OPT_WMM |
Value:
Definition at line 85 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 59 of file weak_memory.h.
◆ OPT_WMM_LIMITS
| #define OPT_WMM_LIMITS |
Value:
"(max-var):" \
"(max-po-trans):"
Definition at line 66 of file weak_memory.h.
◆ OPT_WMM_LOOPS
| #define OPT_WMM_LOOPS |
Value:
"(force-loop-duplication)" \
"(no-loop-duplication)"
Definition at line 70 of file weak_memory.h.
◆ OPT_WMM_MEMORY_MODEL
| #define OPT_WMM_MEMORY_MODEL "(mm):" |
Definition at line 57 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 74 of file weak_memory.h.
Function Documentation
◆ introduce_temporaries()
| void introduce_temporaries | ( | value_setst & | value_sets, |
| symbol_tablet & | symbol_table, | ||
| const irep_idt & | function, | ||
| goto_programt & | goto_program, | ||
| 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 & | value_sets, | ||
| goto_modelt & | goto_model, | ||
| 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 & | message_handler, | ||
| bool | ignore_arrays | ||
| ) |
Definition at line 106 of file weak_memory.cpp.
