Запись в трубу блоков в некоторых случаях

Question

Я пытаюсь установить двустороннюю связь между родителями и детьми, используя каналы, в частности, между моим процессом и решателем smt (Z3).Мой код (в OCaml), кажется, работает во многих случаях, но иногда запись из моего процесса в решатель блокирует.

Кстати, если вам понадобится помощь в чтении кода OCaml, документации по функциям Unix-функций OCaml, которую яиспользуется можно найти здесь: http://ocaml -batteries-team.github.io / батареи в комплекте / 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 question;flush cout

Рабочий процесс заключается в том, что я отправляю запрос решателю, получаю ответ, а затем, в зависимости от ответа, могу отправить ему другой запрос или нет (к сожалению, довольно сложно включить код для этого),Во многих случаях это сработало хорошо, мне удалось сделать кое-что с решателем.Я пробовал довольно большой пример, и хотя я могу отправить (огромный) запрос решателю, а затем прочитать ответ, когда я пытаюсь отправить второй (который, кстати, меньше по размеру, чем первый) запросписать блоки.Если я попытаюсь отправить небольшую строку, она будет работать, или если я разделю новый запрос на два, первая половина не будет заблокирована, а вторая половина заблокирована.

Кажется, решатель почему-то прекратил чтение.Я также выкладываю все в отдельный текстовый файл, с которым Z3 справляется на отлично, без сбоев или чего-либо еще.Как мне подойти к отладке этого?

РЕДАКТИРОВАТЬ: Основываясь на ответе Госвина фон Бредерлоу, я думаю, что я примерно понимаю, почему это происходит.Я задаю огромный запрос, но я не прошу, чтобы решатель что-то сделал, я просто посылаю ограничения.Затем я отправляю еще одно ограничение, требующее, чтобы решатель решил его, и блокировал ожидание ответа, который не был немедленным.Все это прекрасно работает, потому что родитель и решатель не пытаются говорить в одно и то же время.Проблема заключается в том, что когда я запрашиваю модель, куда я отправляю несколько запросов, на которые решатель отвечает сразу (мне не нужно явно запрашивать ответ в конце), и пока я все еще отправляю запросы, решательотправив обратно ответы.Я думал, что так как решатель читает из канала, он должен очиститься, но я, вероятно, пишу быстрее, чем решатель может прочитать и обработать данные канала.Я мог бы использовать неблокирующий ввод-вывод, но это, вероятно, потребовало бы, чтобы я испортил логику моей программы.Я попытаюсь порождать другой поток либо для записи (и, следовательно, основной процесс продолжается, пока не достигнет той части, где начинается чтение из решателя), либо для порождения другого потока для чтения непосредственно перед началом записи.

Answer 1

Обычно существует две проблемы связи с каналами:

1) Как отметил Джеффри Скофилд в своем ответе, вывод в канал не сбрасывается, поэтому он никогда не записывается в канал.Это происходит только с буферизованным вводом-выводом, но это те каналы ocamls.

2) Обе стороны пытаются писать в канал и блокировать, чтобы никто не удосужился прочитать.Это классический тупик.

Кажется, что решатель почему-то прекратил чтение.

Когда вы очищаете свой конец канала, кажется, что он указывает на второйдело в том, проблема.Вы кормите решателя проблемами и заполняете буфер труб.Таким образом, ваш процесс блокирует ожидание решателя для чтения из канала.С другой стороны, решатель записывает информацию, прогресс или решения, а также заполняет буфер других каналов.Теперь он заблокирован, ожидая, что вы прочитаете результат.Классический тупик.

Использование высокоуровневых каналов. Боюсь, что может быть только одно решение.Создайте второй поток, чтобы прочитать обратно вывод.В качестве альтернативы можно использовать низкоуровневый API для файловых дескрипторов и установить неблокирование main_out или использовать асинхронный ввод-вывод, подобный тому, который предоставляется LWT.

Answer 2

Обычная проблема с использованием каналов для связи с процессом, написанным кем-то другим, состоит в том, что их код не очищает вывод в соответствующие моменты. Вы сбрасываете свои результаты, но есть большая вероятность, что решатель не делает то же самое. Обычное поведение Unix stdio - не сбрасывать вывод по строкам, если вывод не идет в терминал (не в канал).

Это может помочь увидеть команду, которую вы вводите для запуска решателя. Если это не процесс, который вы написали сами, я бы сказал, что это может быть проблемой.