z3-408.2: Bindings for the Z3 Theorem Prover
Copyright(c) 2010-2011 Bas van Dijk & Roel van Dijk
LicenseBSD3
MaintainerIago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Safe HaskellSafe-Inferred
LanguageHaskell2010

Z3.Lock

Description

A minimal implementation of a re-entrant lock, adopted from https://github.com/basvandijk/concurrent-extra

Synopsis

Documentation

newtype Lock Source #

A lock is in one of two states: "locked" or "unlocked".

Constructors

Lock 

Fields

Instances

Instances details
Eq Lock Source # 
Instance details

Defined in Z3.Lock

Methods

(==) :: Lock -> Lock -> Bool #

(/=) :: Lock -> Lock -> Bool #

new :: IO Lock Source #

Create a lock in the "unlocked" state.

acquire :: Lock -> IO () Source #

Acquires the Lock. Blocks if another thread has acquired the Lock.

acquire behaves as follows:

  • When the state is "unlocked" acquire changes the state to "locked".
  • When the state is "locked" acquire blocks until a call to release in another thread wakes the calling thread. Upon awakening it will change the state to "locked".

There are two further important properties of acquire:

  • acquire is single-wakeup. That is, if there are multiple threads blocked on acquire and the lock is released, only one thread will be woken up. The runtime guarantees that the woken thread completes its acquire operation.
  • When multiple threads are blocked on acquire, they are woken up in FIFO order. This is useful for providing fairness properties of abstractions built using locks. (Note that this differs from the Python implementation where the wake-up order is undefined.)

release :: Lock -> IO () Source #

release changes the state to "unlocked" and returns immediately.

Note that it is an error to release a lock in the "unlocked" state!

If there are any threads blocked on acquire the thread that first called acquire will be woken up.

wait :: Lock -> IO () Source #

  • When the state is "locked", wait blocks until a call to release in another thread changes it to "unlocked".
  • wait is multiple-wakeup, so when multiple waiters are blocked on a Lock, all of them are woken up at the same time.
  • When the state is "unlocked" wait returns immediately.

wait does not alter the state of the lock.