weak_memory.h File Reference

Weak Memory Instrumentation for Threaded Goto Programs. More...

#include "wmm.h"
#include <util/irep.h>

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:

  " {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:

  OPT_WMM_MEMORY_MODEL                                                         \
  OPT_WMM_INSTRUMENTATION_STRATEGIES                                           \
  OPT_WMM_LIMITS                                                               \
  OPT_WMM_LOOPS                                                                \
  OPT_WMM_MISC

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.