master-degree-notes/Concurrent Systems/test/Untitled.md

GLOB_MUTEX, W_MUTEX, PR_MUTEX and R_MUTEX semaphores init. at 1
R a shared register init. at 0

begin_read() :=
	PRR_MUTEX.down()
	R_MUTEX.down()
	R++ # currently active readers
	if R = 1 then
		PRW_MUTEX.down()
		GLOB_MUTEX.down()
	R_MUTEX.up()
	PRR_MUTEX.up()
	return

end_read() :=
	R_MUTEX.down()
	R--
	if R = 0 then
		GLOB_MUTEX.up()
		PRW_MUTEX.up()
	R_MUTEX.up()
	return

begin_write() :=
	PRR_MUTEX.down()
	PRW_MUTEX.down()
	PRW_MUTEX.up()
	GLOB_MUTEX.down()
	return

end_write() :=
	PRR_MUTEX.up()
	GLOB_MUTEX.up()
	return

monitor RW_READERS :=
	AR, WR, AW, WW, R_batch init at 0
	condition CR, CW

operation begin_read() :=
	WR++
	if (WW || AW != 0 then
		CR.wait()
		CR.signal()
	AR++
	WR--

operation end_read() :=
	AR--
	if AR = 0 then
		CW.signal()

operation begin_write() :=
	WW++
	if (AR + AW != 0) then
		CW.wait()
	AW++
	WW--

operation end_write() :=
	AW--
	if WR > 0 then
		CR.signal()
	else
		CW.signal()