No contexto do STM, como é conceitualmente um log de transações e como ele evolui quando a transação é bem-sucedida após algumas tentativas?

Uma transação STM é executada completamente, registrando cada evento em um log, e a consistência é verificada no final para decidir se a transação deve ser confirmada ou não.

Então, para o seu exemplo de transação

do
  wa <- readTVar ma
  wb <- readTVar mb
  writeTVar ma (Set.delete win wa)
  writeTVar mb (Set.insert win wb)

Cada tentativa é executada uma readTVarúnica writeTVarvez. Essas funções gravam em um log, que registra se cada evento é uma leitura ou gravação, o TVar afetado e o valor lido ou gravado.

READ ma a   -- value a is read from ma (note that values are just pointers as far as STM is concerned)
READ mb b   -- value b is read from mb
WRITE ma c  -- value c is written to ma
WRITE mb d  -- value d is written to mb

Durante essa transação, outras threads podem confirmar transações que gravam nos mesmos TVars. A transação atual continua, independentemente disso.

Quando atomicallytermina de executar uma transação, ele bloqueia todos os TVars que aparecem em seu log para garantir que o que se segue aconteça atomicamente:

• atomicallyverifica se os valores lidos no log correspondem aos valores atuais nos TVars, o que significa que eles não foram substituídos (ou outra transação escreveu o mesmo valor no TVar, o que é bom).

• Se o log corresponder aos TVars, os eventos de gravação serão aplicados aos respectivos TVars. É isso que significa "commit" a transação. Os bloqueios são liberados e atomicallyretornados.

• Caso contrário, há uma incompatibilidade entre o log e o conteúdo de um TVar; o log é descartado, os bloqueios são liberados e atomicallyreinicia do início.

No seu exemplo, se houve três tentativas, significa que foram criados três logs completos semelhantes aos acima. A única diferença entre os dois primeiros é que, ao atomicallyanalisar esses logs novamente, não foi possível fingir que eles ocorreram atomicamente, então a transação foi reiniciada.

Acredito que algo assim serviria como um modelo mental bastante decente:

data Generational a = Generational
    { generation :: Int
    , value :: a
    }
instance Eq (Generational a) where (==) = (==) `on` generation

-- choose a generation number that's never been chosen before
-- e.g. by starting at minBound and incrementing one at each call
freshGeneration :: IO Int

newtype TVar a = TVar (IORef (Generational a))

unsafeReadTVar :: MonadIO m => TVar a -> m (Generational a)
unsafeReadTVar (TVar ref) = liftIO $ readIORef ref

unsafeWriteTVar :: Int -> TVar a -> Identity a -> IO ()
unsafeWriteTVar g (TVar ref) (Identity a) = writeIORef ref (Generational g a)

lock, unlock :: TVar a -> IO ()

-- like Map, but with an extra type argument
data Map1 (key :: k -> *) (value :: k -> *)

data STMLog = STMLog
    { reads :: Map1 TVar Generational
    , writes :: Map1 TVar Identity
    }

emptyLog :: STMLog
emptyLog = STMLog empty1 empty1

-- throw away the generation
readsId :: STMLog -> Map1 TVar Identity
readsId = fmap1 (Identity . value) . reads

newtype STM a = STM (StateT STMLog IO a)
    deriving (Functor, Applicative, Monad)

readTVar :: TVar a -> STM a
readTVar v = STM do
   log <- get
   case lookup1 v (writes log) <|> lookup1 v (readsId log) of
        Just (Identity a) -> pure a
        Nothing -> do
            ga <- unsafeReadTVar v
            put log { reads = insert1 v ga (reads log) }
            pure (value ga)

writeTVar :: TVar a -> a -> STM ()
writeTVar v a = STM $ modify \log ->
    log { writes = insert1 v (Identity a) (writes log) }

atomically :: STM a -> IO a
atomically (STM act) = do
    (a, log) <- runStateT act emptyLog
    let allVars = keys1 $ union1 (readsId log) (writes log)
    traverse1_ lock allVars
    reads' <- traverseWithKey1 (\v _ -> unsafeReadTVar v) (reads log)
    -- N.B. (==) only compares generations here
    -- (the real implementation probably uses some form
    -- of pointer equality instead of storing generations)
    if reads log == reads'
        then do
            g <- freshGeneration
            traverseWithKey1_ (unsafeWriteTVar g) (writes log)
            traverse1_ unlock allVars
            pure a
        else do
            traverse1_ unlock allVars
            atomically (STM act) -- try again

A coisa real é provavelmente um pouco mais complicada/otimizada/robusta. Não vou me preocupar em lidar com exceções aqui, estou assumindo que bloquear uma coleção de variáveis ​​de uma só vez é fácil, não estou mostrando a implementação de retry, não pensei se alguma cerca de memória é necessária, etc.