I got E08255 UNPROVABLE_LOCK_ORDER — why are two locks of the same type rejected even with no reverse nesting?

← Concurrency · Ref: Q1352

E08255 fires when two locks of the SAME type — held on caller-supplied objects — are nested, even if only ONE nesting direction appears in the code. Because the two objects (`from` and `to` here) are interchangeable at the call site, a single static `from` then `to` ordering can instantiate at runtime as both `A,B` and `B,A`. The compiler cannot PROVE a consistent global order, so it rejects the nesting.

WHAT THE ERROR MEANS

Unlike E08252 (two distinct lock fields, provably orderable), here both locks are `theLock` reached through same-type parameters. `moveFunds(x, y)` and `moveFunds(y, x)` both type-check, so nesting `to` inside `from` is simultaneously both acquisition orders — the classic bank-transfer / dining-philosophers deadlock.

HOW TO FIX

Don't nest same-type locks. Acquire them one at a time, or put the shared payload under a SINGLE MutexLock of an owning record so only one lock is ever taken.

  require from.getLock().enter(fromKey)   //completes and releases
  require to.getLock().enter(toKey)        //separate, unnested

WHY EK9 DETECTS THIS

Same-type nested locks are the textbook deadlock (two accounts, two philosophers). Runtime ordering tricks (lock by hashcode) are error-prone; EK9 rejects the shape at compile time.

Example

defines module qa.concurrency.unprovable.lock.order

  defines class

    Vault
      theLock as MutexLock of Integer: MutexLock(Integer(0))
      getLock() as pure
        <- rtn as MutexLock of Integer: theLock
      default operator ?

  defines function

    moveFunds()
      ->
        from as Vault
        to as Vault
      fromKey <- () is MutexKey of Integer as function
        stdout <- Stdout()
        stdout.println(lockedItem)
      require from.getLock().enter(fromKey)

      toKey <- () is MutexKey of Integer as function
        stdout <- Stdout()
        stdout.println(lockedItem)
      require to.getLock().enter(toKey)

Common mistakes

E08255 — Both locks are `theLock` reached through same-type params `from`/`to`, which are interchangeable at the call site, so nesting `to` inside `from` instantiates as both orders at runtime — an unprovable order. Fix by acquiring sequentially or unifying under one MutexLock of a record. See ek9 -h E08255.

Incorrect:

innerKey <- () is MutexKey of Integer as function
        stdout <- Stdout()
        stdout.println(lockedItem)
      outerKey <- (to, innerKey) is MutexKey of Integer as function
        require to.getLock().enter(innerKey)
      require from.getLock().enter(outerKey)

Correct:

fromKey <- () is MutexKey of Integer as function
        stdout <- Stdout()
        stdout.println(lockedItem)
      require from.getLock().enter(fromKey)

      toKey <- () is MutexKey of Integer as function
        stdout <- Stdout()
        stdout.println(lockedItem)
      require to.getLock().enter(toKey)

Coming from another language?

Java: the canonical fix is to lock by System.identityHashCode ordering — easy to get wrong, invisible if wrong. EK9: nesting two same-type locks reached via interchangeable objects is a compile-time error (E08255); unify under one lock or acquire sequentially.

Keywords: type, deadlock, order, instance, philosophers, lock, same, transfer, nested, MutexLock, concurrent, unprovable, E08255