goto_atomicity_check.h File Reference

#include <goto-programs/goto_functions.h>
#include <util/symtab/context.h>
#include <util/symtab/namespace.h>

Include dependency graph for goto_atomicity_check.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	goto_atomicity_check (goto_functionst &goto_functions, const namespacet &ns, contextt &context)
	Post-GOTO-conversion atomicity check instrumentation pass.

Function Documentation

goto_atomicity_check()

void goto_atomicity_check	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		contextt &	context )

Post-GOTO-conversion atomicity check instrumentation pass.

For each assignment to or read from a global variable, inserts:

• Snapshot assignments: tmp_i = global_i
• If the LHS is also a global: ATOMIC_BEGIN ... ATOMIC_END wrapping
• An assertion: assert(tmp_i == global_i) checking for concurrent modification between the snapshot and the assignment.

This corresponds to the –atomicity-check flag and detects violations of atomicity when multiple threads access shared global variables.