在某些情况下写入管道块

Posted 2023-02-16

【中文标题】在某些情况下写入管道块

【英文标题】：Writing to pipe blocks in some cases

【发布时间】：2019-01-24 01:33:59

【问题描述】：

我正在尝试使用管道建立双向父子通信，特别是在我的进程和 smt 求解器 (Z3) 之间。我的代码（在 OCaml 中）似乎在许多情况下都可以工作，但有时从我的进程写入求解器会阻塞。

顺便说一句，如果您在阅读 OCaml 代码时需要一些帮助，我使用的 OCaml unix 函数的文档可以在这里找到： http://ocaml-batteries-team.github.io/batteries-included/hdoc2/BatUnix.html

let (solver_in, main_out) = BatUnix.pipe ~cloexec:false () in
(* pipe that solver writes to and parent reads from *)
let (main_in, solver_out) = BatUnix.pipe ~cloexec:false () in

(* Solver should not get the descriptors used by parent to read and write *)
BatUnix.set_close_on_exec main_in;
BatUnix.set_close_on_exec main_out;

let pid = BatUnix.create_process solver (Array.of_list (solver :: params))
          solver_in solver_out solver_out in

(* Parent should close the descriptors used by the solver *)
BatUnix.close solver_in;
BatUnix.close solver_out;
let cin = Unix.in_channel_of_descr main_in in
set_binary_mode_in cin false;
let cout = Unix.out_channel_of_descr main_out in
set_binary_mode_out cout false

这是我用来写入求解器管道的代码： output_string cout 问题； 同花顺

所涉及的工作流程是我向求解器发送一个查询，得到一个答案，然后根据答案，我可能会向它发送另一个查询或不发送另一个查询（不幸的是，这很难包含代码）。在许多情况下，这运作良好，我已经设法用求解器来回做了一些。 我正在尝试一个非常大的示例，虽然我可以向求解器发送一个（巨大的）查询，然后阅读回复，但当我尝试发送第二个（顺便说一下，它的大小比第一个小）时，查询写块。如果我尝试发送一个小字符串，它将起作用，或者如果我将新查询分成两部分，前半部分不会被阻塞，但后半部分会被阻塞。

求解器似乎由于某种原因已停止读取。我还在一个单独的文本文件中吐出所有内容，Z3 处理得很好，没有崩溃或任何东西。我该如何调试呢？

编辑：根据 Goswin von Brederlow 的回答，我想我可以大致了解为什么会发生这种情况。我正在提供一个巨大的查询，但我并没有要求求解器做任何事情，我只是发送约束。然后我再发送一个约束，要求求解器解决它，并阻止等待不是立即的答案。这一切都很好，因为父母和求解器并没有试图在同一时间交谈。 问题是当我询问模型时，我发送一堆查询，求解器立即回答（我不必在最后明确要求答案），而当我仍在发送查询时，求解器是发回答案。我在想，由于求解器正在从管道中读取它应该清除，但我的写入速度可能比求解器读取和处理管道数据的速度要快。我可以使用非阻塞 IO，但这可能需要我弄乱程序的逻辑。我将尝试生成另一个线程来进行写入（因此主进程会继续，直到它到达它开始从求解器读取的部分）或者在开始写入之前生成另一个线程来读取。

【参考方案1】：

与管道通信通常有两个问题：

1) 正如 Jeffrey Scofield 在他的回答中提到的那样，管道的输出没有被刷新，因此它从未真正写入管道。这只发生在缓冲 IO 上，但这就是 ocamls 通道。

2) 双方都尝试写入管道并阻塞，因此没有人可以阅读。这是一个典型的僵局。

求解器似乎由于某种原因停止读取。

当您冲洗管道末端时，这似乎表明第二种情况是问题所在。您正在为求解器提供问题并已填充管道缓冲区。因此，您的进程会阻塞等待求解器从管道中读取数据。另一方面，求解器正在写回信息、进度或解决方案，并且还填充了其他管道缓冲区。它现在被阻止等待您读回输出。典型的僵局。

恐怕使用高级渠道可能只有一种解决方案。创建第二个线程以读回输出。替代方法是使用文件描述符的低级 API 并将 main_out 设置为非阻塞或使用 LWT 提供的异步 IO。

【讨论】：

我想我明白为什么会发生 2。在第一种情况下，即使我提供了一个巨大的查询，我也没有要求求解器做任何事情，我只是发送约束。然后我再发送一个约束，要求求解器解决它，并阻止等待答案。这一切都很好，因为父级和求解器并没有试图在同一时间交谈。

【参考方案2】：

使用管道与其他人编写的进程进行通信的常见问题是他们的代码不会在适当的时候刷新输出。您正在刷新您的输出，但求解器很可能没有做同样的事情。 Unix stdio 的通常行为是不按行刷新输出，除非输出到终端（不是管道）。

查看您发出的用于启动求解器的命令可能会有所帮助。如果这不是您自己编写的过程，我会说这很可能是问题所在。

【讨论】：

这是启动求解器的命令：let pid = BatUnix.create_process solver (Array.of_list (solver :: params)) solver_in solver_out solver_out in