CPS, π, actors, event loop

[sassa_nf]

I have joined my current company to get better exposure to CPS, actors, event-driven programming. What I have found is that strict reasoning about the program's correctness requires a lot more effort: things that would be guaranteed by program order, are no longer guaranteed; more over, new things can happen apparently concurrently, in what

Comments

[zeit_raffer]

Вместо актора, который ожидает все команды, нужен актор, который ожидает первую и превращается в актора, который ожидает вторую и т.д.

[zeit_raffer]

То есть в терминах акторов такое общепринято. А event-driven хз

[ex_juan_gan]

Это более похоже на π.

[sassa_nf]

ну тут, возможно, ближе, что каждый из event handlers - это и есть актор. Таким образом, в принципе, можно прицепить on('rcpt', ...) внутри обработки on('mail', ...). Но от конкурентности X, Y, Z избавиться не так легко.

Более того, появление Z, скорее всего, более детерминистично, чем кажется, но из одной "сигнатуры" этого нельзя заключить.

[ex_juan_gan]

Good observation.

I believe, if you are dealing with time, the isomorphism between A and (A→⊥)→⊥ does not exist. The logic is not boolean.

Which does not eliminate the rest of your story. Life is hard.

[sassa_nf]

But what does become simpler with actors? :-)

"the isomorphism between A and (A→⊥)→⊥ does not exist"

yes, this is a long-standing question for me. I've read somewhere CPS is "isomorphic" to "direct" style, but it is not clear in what sense that is true. But probably I should just forget about it. Having tried a taste of intuitionism it is hard to imagine that statement to ever be true. :-)

[nivanych]

Акторы (ну или пи), это низкий уровень, это база, вокруг которой можно строить остальное.
Что-то отдельное, может быть, они упростят, но не более того.

Немало такой хрени, это что-то, похожее на клиент-сервер, и во всяком случае, записываемое, как общение двух автоматов достаточно простого вида.
Насколько я видел, первая общеизвестная попытка использовать подобные соображения, это CSP.
Мне оно не очень нравится, но что несомненно - reasoning про поведения процессов там by design. Ну и описание всяких там "SMTP" там упрощается, это точно.

complexity introduced by event-driven style

[nponeccop]

Это дурацкий вопрос. Event-driven никакой сложности не добавляет, это у вас протокол вырожден и есть очевидный "золотой" путь через FSM, который вы можете в многопоточном случае выразить через неявное состояние в control flow, и в каждом состоянии допустимы всего пара сообщений.

Для вырожденных протоколов есть coroutines/yield, позволяющие записать код в стиле "SMTP server without CPS" в ноде.

Для невырожденных придется использовать формализацию протокола в виде грамматики или стейт-машины.

Стейт-машина проще - есть "пользовательская" функция (state, message) -> state, представляющая из себя кейс по стейтам и мессаджам, и есть "библиотечный" парсер протокола, который её в цикле вызывает.

Для начала нарисуйте ваш протокол в dot, типа https://en.wikipedia.org/wiki/Finite-state_machine#/media/File:Turnstile_state_machine_colored.svg

Re: complexity introduced by event-driven style

[sassa_nf]

Нет, не дурацкий вопрос :-)

Для FSM все равно нужно "вошел в rcpt to" - "вышел из rcpt to". А когда у нас "вышел из rcpt to"? В direct style переход между состояниями разграничен by program order и такого понятия как "вышел из rcpt to" в явном виде нет.

В CPS понадобится композиция "вышел из rcpt to" в хвост или "на дно" всей пирамиды of doom - теперь нужно "вышел из rcpt to" всобачить явно. Без этого нужно ограничиться более слабым утверждением, на котором строить корректность: "вошел в rcpt to и выполнил X statements до первого асинхрона".

Далее, X, Y, Z в указанном примере находятся в частях системы с неизвестной implementation-specific связью. Опять, нужно программировать в стиле, опирающемся на более слабые утверждения о порядке X, Y, Z.

Еще далее: occurrence of error не имеет каузальной связи с "вошел в rcpt to и пока еще не вышел из rcpt to". Это совсем не дурацкие вопросы :-)

Re: complexity introduced by event-driven style

[sassa_nf]

"представляющая из себя кейс по стейтам и мессаджам"

о, а кстати. case msg of 'rcpt' -> X (которые в цикле вызывается) сильно отличается от smtp.on('rcpt', X)? Мне не очевидно.

Проблема, стало быть, как раз в том, что все остальное в CPS стиле тоже. Нет очевидного program order, устанавливающего темпоральные связи; нет даже порядка нормализации, устанавливающего data dependency связи. Отсюда, например, проблема, что X, Y, Z появляются в неопределенном порядке. Особенно Z. В direct style ошибки появляются в каузальном порядке - я вызвал read, получил отлуп. В event-driven эта связь пропадает.

Re: complexity introduced by event-driven style

[nponeccop]

Вот базовая архитектура, от которой отталкиваемся:

https://gist.github.com/nponeccop/446b0547f3942be0f41b51105c4b02d2

patterns концептуально - тот же events.emit, только с multiple dispatch (в принципе можно целый DSL паттернов забацать).

handle вызывается парсером протокола. Парсер же обрабатывает переход в состояние done специальным образом.

Можем этот код расширить до размера, иллюстрирующего проблему.

X Y Z в моем дизайне не могут появиться в неопределённом порядке, поскольку порядок гарантируется стейт машиной.

А запись порядка в стейт машине вам понадобится в 99% случаев, поскольку в 99% случаев есть нондетерминизм в самом протоколе, который program order не опишешь.

И для гарантирования порядка в прямых цепочках в любом случае есть

foo
.then(() => ...)
.then(...)
.done()Но как я сказал выше, это не работает почти никогда.