Fondazione Bruno Kessler Universitá	 di Bologna Computer Science Department INRIA Rever
CaReDeb

μOz is a higher-order language featuring thread-based concurrency and asynchronous communication via channels.

μOz Syntax
Program	=		S
S		= 		S ; S							sequence
			|	let id = v in S end				assignment
			| 	if bool_exp then S else S end		condition
		 	|	thread S end					thread creation	
			|	skip							nil
			|	{id var_list}					procedure call
			|	{send x y}					message send
			|	assert bool_exp				assertion
			
var_list 	= 		0 | id var_list					parameter list

v		= 		true						
			|	false
			|	{receive x}					reading from channel x
			|	proc { var_list } S end			procedure declaration
			|	port 							channel creation
			|	int_exp

bool_exp	=		bool							boolean expressions
			|	(int_value > int_value)	|	(int_value < int_value)
			|	(int_value >= int_value)	|	(int_value <= int_value)
			|	(int_value == int_value)

bool		=		true | false | id

int_exp	=		int_value						integer expressions
			|	int_value + int_exp
			|	int_value - int_exp
			| 	int_value / int_exp
			|	int_value * int_exp

int_value	=		number | id
μOz examples

Concurrency Bugs

These are examples highlighting paradigmatic concurrency bugs: