9

我有一些应用程序架构，其中用户输入流向一些自动机，它在事件流的上下文中运行并将用户引导到应用程序的不同部分。应用程序的每个部分都可以根据用户输入运行一些操作。但是，应用程序的两个部分共享一些状态，并且在概念上是读取和写入相同的状态。需要注意的是，两个“线程”没有同时运行，其中一个“暂停”，而另一个“产生”输出。描述这种状态共享计算的规范方法是什么，而不使用一些全局变量？两个“线程”保持通过某种形式的消息传递同步的本地状态是否有意义，即使它们无论如何都不是并发的？

由于问题更具概念性，因此没有代码示例，但欢迎使用 Haskell（使用任何 FRP 框架）或其他语言中的示例回答。

4

1 回答 1

14

我一直在努力解决这个问题。高级摘要是您：

A) 将所有并发代码提炼成纯单线程规范

B) 单线程规范用于StateT共享公共状态

整体架构受到模型-视图-控制器的启发。你有：

  • 控制器，它们是有效的输入
  • 视图，这是有效的输出
  • 一个模型，它是一个纯流转换

模型只能与一个控制器和一个视图交互。但是，控制器和视图都是 monoid，因此您可以将多个控制器组合成一个控制器，将多个视图组合成一个视图。从图形上看，它看起来像这样：

 controller1 -                                           -> view1
              \                                         /
 controller2 ---> controllerTotal -> model -> viewTotal---> view2
              /                                         \
 controller3 -                                           -> view3

                  \______ ______/   \__ __/   \___ ___/
                         v             v          v
                     Effectful        Pure    Effectful

该模型是一个纯粹的单线程流转换器，它实现Arrow和ArrowChoice. 原因是这样的：

  • Arrow是单线程等价于并行
  • ArrowChoice是单线程等价于并发

在这种情况下，我使用 push-based pipes，它似乎有一个正确的Arrow实例ArrowChoice，尽管我仍在努力验证法律，所以这个解决方案仍然是实验性的，直到我完成他们的证明。对于那些好奇的人，相关的类型和实例是：

newtype Edge m r a b = Edge { unEdge :: a -> Pipe a b m r }

instance (Monad m) => Category (Edge m r) where
    id = Edge push
    (Edge p2) . (Edge p1) = Edge (p1 >~> p2)

instance (Monad m) => Arrow (Edge m r) where
    arr f = Edge (push />/ respond . f)
    first (Edge p) = Edge $ \(b, d) ->
        evalStateP d $ (up \>\ unsafeHoist lift . p />/ dn) b
      where
        up () = do
            (b, d) <- request ()
            lift $ put d
            return b
        dn c = do
            d <- lift get
            respond (c, d)

instance (Monad m) => ArrowChoice (Edge m r) where
    left (Edge k) = Edge (bef >=> (up \>\ (k />/ dn)))
      where
          bef x = case x of
              Left b -> return b
              Right d -> do
                  _ <- respond (Right d)
                  x2 <- request ()
                  bef x2
          up () = do
              x <- request ()
              bef x
          dn c = respond (Left c)

该模型还需要是一个单子变压器。原因是我们想嵌入StateT基础 monad 来跟踪共享状态。在这种情况下，pipes符合要求。

难题的最后一块是一个复杂的现实世界示例，它采用复杂的并发系统并将其提炼成纯单线程等价物。为此，我使用我即将推出rcpl的库（“read-concurrent-print-loop”的缩写）。该rcpl库的目的是为控制台提供一个并发接口，使您可以在同时打印到控制台的同时读取用户的输入，但打印的输出不会破坏用户的输入。它的 Github 存储库在这里：

链接到 Github 存储库

我最初对该库的实现具有普遍的并发性和消息传递，但受到几个我无法解决的并发错误的困扰。然后当我想出mvc（我的类似 FRP 的框架的代号，“model-view-controller”的缩写）时，我认为这rcpl将是一个很好的测试用例，看看是否mvc准备好迎接黄金时段。

我把整个逻辑rcpl变成了一个单一的、纯粹的管道。这就是您将在本模块中找到的内容，整个逻辑完全包含在rcplCore管道中。

这很简洁，因为现在实现是纯粹的，我可以快速检查它并验证某些属性！例如，我可能想要快速检查的一个属性是，每次用户按键都只有一个终端命令x，我会这样指定：

>>> quickCheck $ \n -> length ((`evalState` initialStatus) $ P.toListM $ each (replicate n (Key 'x')) >-> runEdge (rcplCore t)) == n || n < 0

n是我按键的次数x。运行该测试会产生以下输出：

*** Failed! Falsifiable (after 17 tests and 6 shrinks):
78

QuickCheck 发现我的财产是假的！此外，由于代码是引用透明的，QuickCheck 可以将反例缩小到最小再现违规。按下 78 键后，终端驱动程序会发出一个换行符，因为控制台是 80 个字符宽，并且提示占用了两个字符（"> "在这种情况下）。IO如果并发并感染了我的整个系统，我将很难验证这种属性。

有一个纯粹的设置是伟大的另一个原因：一切都是完全可重现的！如果我存储所有传入事件的日志，那么只要有错误，我就可以重播这些事件，并拥有完美再现的测试用例，我可以将其添加到我的测试套件中。

然而，纯度真正最重要的好处是能够更轻松地以非正式和正式方式推理代码。当您从等式中删除 Haskell 的调度程序时，您可以静态地证明您的代码在必须依赖具有非正式指定语义的并发运行时时无法证明的事情。这实际上被证明是非常有用的，即使对于非正式的推理，因为当我转换我的代码以使用mvc它时仍然有几个错误，但这些比我第一次迭代中顽固的并发错误更容易调试和删除。

该rcpl示例用于StateT在不同组件之间共享全局状态，因此对您的问题的冗长回答是：您可以使用StateT，但前提是您将系统转换为单线程版本。幸运的是，这是可能的！

于 2013-10-06T00:49:05.143 回答