[BUG]: STM: opacity

[durban]

Version

1.0-RC1

Scala Version

3.7.0

Expected Behavior

Expected that I can never observe an inconsistent view of memory. Please see previous discussion in #1158.

Actual Behavior

I can sometimes oberve an inconsistent view of memory, i.e., something that no transaction ever committed.

Steps to Reproduce

import kyo.{ <, KyoApp, STM, TRef, Async, Sync }

object Repro extends KyoApp {
  run {
    for {
      // initially they contain equal values:
      r1 <- STM.run(TRef.init("a"))
      r2 <- STM.run(TRef.init("a"))
      txn1 = for {
        v1 <- r1.get
        v2 <- r2.get
        // we only write equal values:
        _ <- r1.set(v1 + "1")
        _ <- r2.set(v2 + "1")
      } yield ()
      txn2 = {
        def txn2: Unit < STM = r1.get.map[Unit, STM] { v1 =>
          r2.get.map { v2 =>
            if (v1 == v2) {
              ()
            } else {
              // Observed non-equal values. Now, this transaction
              // will never commit (which is correct, since it is
              // based on an inconsistent view of memory); however
              // SOMETIMES this occurrence is observable "outside":
              txn2
            }
          }
        }
        txn2
      }
      once = Async.zip(STM.run(txn1), STM.run(txn2)).map { _ =>
        Sync.defer { println("ok") }
      }
      _ <- Async.foreachDiscard(1 to 100000, concurrency = 8) { _ => once }
    } yield ()
  }
}

This program prints a lot of ok lines, then stops printing them and hangs.

Please note, that where the Observed non-equal values... comment is, instead of the monadic infinite recursion, we could do a simple infinite loop (i.e., while (true) {}), which is not so simple to fix, because it never gets back to the interpreter.

As noted before in #1158, this is about the STM consistency property called "opacity" in the literature. In short, if the STM engine guarantees opacity, such inconsistencies are never visible to a transaction. The TL2 paper linked there outlines an algorithm which provides opacity. It seems somewhat similar to what kyo-stm uses.

I believe the main difference is that kyo-stm increases the global version-clock (TID) when it starts a speculative execution. However, TL2 does this after locking the write-set (section 2.1 in the paper). I believe this causes the difference in observable inconsistencies.

Current Workaround

Arguably, this could be a "feature request" instead of a "bug". I don't really care how it's classified, I'd just like it to be considered :-)

[fwbrasil]

Thank you for the report! Would you have an example with another STM implementation that is able to provide this level of isolation? It seems intrinsic to optimistic locking when there are multiple value reads.

[durban]

Sure. The mentioned TL2 is one example. Another one is ScalaSTM, which is explicitly documented to provide opacity. The (approximate) equivalent of the example above with ScalaSTM is like this:

import scala.concurrent.stm.{ atomic, Ref, InTxn }
import scala.concurrent.{ Future, Await }
import scala.concurrent.ExecutionContext.Implicits.global
import scala.concurrent.duration._

object Foo {

  def main(args: Array[String]): Unit = {
    // initially they contain equal values:
    val r1 = Ref("a")
    val r2 = Ref("a")

    def txn1(implicit it: InTxn): Unit = {
      val v1 = r1.get
      val v2 = r2.get
      // we only write equal values:
      r1.set(v1 + "1")
      r2.set(v2 + "1")
    }

    def txn2(implicit it: InTxn): Unit = {
      val v1 = r1.get
      val v2 = r2.get
      if (v1 == v2) {
        ()
      } else {
        // Observed non-equal values (never happens)
        println(s"${v1} != ${v2}")
        while (true) {}
      }
    }

    (1 to 100000).foreach { _ =>
      val fut = Future.sequence(Seq(
        Future { atomic(txn1(_)) },
        Future { atomic(txn2(_)) }
      ))
      Await.result(fut, Duration.Inf)
      println("ok")
    }
  }
}

And indeed, this example never hangs.

(I don't think this issue is intrinsic to optimistic locking. At least not in the sense that it would be unfixable. TL2 uses optimistic locking + provides opacity. Another solution in the STM literature is some kind of sandboxing, e.g., Haskell does that I think.)

[fwbrasil]

thank you for the patience and repros 🙏 #1455

[fwbrasil]

fixed by #1455