Fix: Output in JavaScript not consistent #1824

MikaelMayer · 2022-02-14T21:43:11Z

By switching to the asynchronous API of processing output data of process, this PR makes it possible to run the option /compiler:3 and have an output when the compiler is js.

Fix dafny-lang/ide-vscode#131

I don't know how to reproduce this in a test. Reading nodeProcess.StandardOutput.ReadtoEnd() works as well, and without it or without this PR nothing prints to screen.

Note for reviewing:

The event specification says that the callbacks are called after each newline, and do not include the newline (I tested)
However, if the process exited, the callbacks are called with the remaining data.
Therefore, I test if the process exited, and if so, I add a newline after the data, else I just write the data. This seems to works for all of our tests and for my use case.

cpitclaudel · 2022-02-15T01:29:33Z

Source/Dafny/Compilers/Compiler-js.cs

 };

 try {
 using var nodeProcess = Process.Start(psi);
+ nodeProcess.BeginErrorReadLine();
+ nodeProcess.BeginOutputReadLine();


Don't you want to put these after the ProcessOutputData setup?

cpitclaudel · 2022-02-15T01:30:12Z

Source/Dafny/Compilers/Compiler-js.cs

+ } else {
+ Console.Out.Write(e.Data);
+ }
+ }


Remove the duplication by extracting a method

Just to add to @cpitclaudel's suggestion: I wouldn't declare it as an inner method since you don't require any closures.

I did close on on nodeProcess. However, after reading the documentation, it looks like the closure's first argument is the process itself, it just needed to be casted. I removed the duplication by creating a private method,

cpitclaudel · 2022-02-15T01:46:46Z

Should this be equivalent to just not redirecting output at all? I'm confused why it works.

That being said, nodejs does something really weird with IO on Windows. nodejs/node#4697

camrein · 2022-02-15T10:49:12Z

Source/Dafny/Compilers/Compiler-js.cs

+ } else {
+ Console.Out.Write(e.Data);
+ }
+ }


Just to add to @cpitclaudel's suggestion: I wouldn't declare it as an inner method since you don't require any closures.

camrein · 2022-02-15T10:53:37Z

Source/Dafny/Compilers/Compiler-js.cs

+ Console.Out.Write(e.Data);
+ }
+ }
+ nodeProcess.ErrorDataReceived += ProcessErrorData;


Move the registration of the event-handlers before the asynchronous setup BeginErrorReadLine to not miss any process output due to the race condition.

MikaelMayer · 2022-02-15T15:25:21Z

That being said, nodejs does something really weird with IO on Windows. nodejs/node#4697

I think you nailed it ! Yes, it should be equivalent to do no redirection at all, but it is not on Windows for node.js and I don't know why.

camrein

Looks good, just two notes where it's up to your preference.

camrein · 2022-02-15T15:43:53Z

Source/Dafny/Compilers/Compiler-js.cs

@@ -2378,6 +2378,16 @@ protected class ClassWriter : IClassWriter {
 return SendToNewNodeProcess(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, outputWriter);
 }

+ DataReceivedEventHandler ProcessData(TextWriter writer) {
+ return (sendingProcess, e) => {
+ if (!((Process)sendingProcess).HasExited) {


I don't have a strong opinion about this, but I tend to avoid casts where possible. Since you're already providing writer as a closure, you may as well do so for the Process instance. But I leave it up to you.

Thanks for your comment.
I will keep the cast as since the closure is already provided with the process, I don't think that adding it to the closure builder would be beneficial, especially just for having the type.

camrein · 2022-02-15T15:46:48Z

Source/Dafny/Compilers/Compiler-js.cs

@@ -2378,6 +2378,16 @@ protected class ClassWriter : IClassWriter {
 return SendToNewNodeProcess(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, outputWriter);
 }

+ DataReceivedEventHandler ProcessData(TextWriter writer) {


I think you could provide a more descriptive name here. On the one hand it's actually a factory for event handlers, on the other hand the created event handler prints the data to the specified writer.

MikaelMayer · 2022-02-16T18:17:38Z

Whatever I do, I can't properly transfer STDOUT from the child process to the parent. There are unreproducible race conditions between the process having exited and the need to guess that a line ending triggered e.Data was sent. The last newline might or might not be taken into account.

Hence, I'm completely removing this solution and replace it with a simple one where two while loops take care of transferring the process's output to current process's output, character by character.

cpitclaudel · 2022-02-16T18:47:12Z

Source/Dafny/Compilers/Compiler-js.cs

+ }
+ while ((current = nodeProcess.StandardError.Read()) != -1) {
+ Console.Error.Write((char)current);
+ }


I don't think this is safe, the process may fill the stderr buffer and block on it while we wait for stdout.

From https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.process.standardoutput?view=net-6.0:

Synchronous read operations introduce a dependency between the caller reading from the StandardOutput stream and the child process writing to that stream. These dependencies can result in deadlock conditions. When the caller reads from the redirected stream of a child process, it is dependent on the child. The caller waits on the read operation until the child writes to the stream or closes the stream. When the child process writes enough data to fill its redirected stream, it is dependent on the parent. The child process waits on the next write operation until the parent reads from the full stream or closes the stream. The deadlock condition results when the caller and child process wait on each other to complete an operation, and neither can proceed. You can avoid deadlocks by evaluating dependencies between the caller and child process.

I pushed something so that the error writing is done in a different thread. I think it solves the deadlock problem. Let me know if you agree with this.

into fix-ide-vscode-131

cpitclaudel · 2022-02-16T21:16:36Z

Source/Dafny/Compilers/Compiler-js.cs

+ int current;
+ while ((current = nodeProcess.StandardOutput.Read()) != -1) {
+ Console.Out.Write((char)current);
+ }


Looks good now, though reading character-by-character is a bit scary. I'm not sure it's that important since it's just a debugging facility, but if it is I would spawn two instances of a class that does something roughly like

while (var count = await ReadAsync(buf, 0, bufsize)) { outputStream.Write(buf) }

IIRC ReadAsync is only blocks until some output is received.

I second that it might be beneficial to not read char by char. However, since the Dafny Compiler consists purely of synchronous methods, I suggest using the non-async version instead (it's discouraged using async APIs in sync code and vice versa).
Either use Read with a buffer or ReadLine. Although, the latter might be not the best choice since we cannot clearly say that the output is always separated by lines.

About character by character vs. buffering.
Buffering is a best practice when the goal is to recover the entire output into some kind of file, or for real-time application processing. Not when it's user-facing.
Here, we are talking about dafny.exe -compile:3 -compileTarget:js, which is a tool mostly used while developing a JavaScript application in Dafny. Its output is mean to be visible by the user, for example in the IDE, else they would just use node on a generated file.
So now, if the output has I/O operations, buffering the output would result in not displaying in real-time the output, which would result in a disastrous user experience.

I refactored the code so that it's now inside a function

camrein · 2022-02-17T11:43:37Z

Source/Dafny/Compilers/Compiler-js.cs

@@ -2401,6 +2404,17 @@ protected class ClassWriter : IClassWriter {
 }
 nodeProcess.StandardInput.Flush();
 nodeProcess.StandardInput.Close();
+ // Fixes a problem of Node on Windows, where Node does not prints to the parent console its standard outputs.
+ Task.Run(() => {


Try to avoid fire-and-forget tasks. Errors happening inside the task will be lost.
Either add an exception handler that prints to the desired output, add a continuation responsible to handle errors, or best: Wait for the task's completion so potential errors are reported back to the main thread. Mind that exceptions that occured inside a task are wrapped by an AggregateException that you may want to unwrap first.

I wait for the result of this task now just after waiting for the process to exit. I will not handle errors at this point because I don't see a use case for that yet.

camrein

I preferred the previous implementation. However, since it appears that there's an unsolvable problematic when catching the final output of a process it's OK to change it according to your suggestion.

camrein

Looks good. Aren't there any test cases for similar cases?

MikaelMayer · 2022-02-17T20:28:12Z

Aren't there any test cases for similar cases?

Yes there are but none of them are able to catch this error and that's obscure to my why.
There is a test for JavaScript, which works because it calls "node" on the shell.
https://github.com/dafny-lang/dafny/blob/master/.github/workflows/release-downloads.yml#L109
However, looking at recent output of the dafny command that is also supposed to run the file, it also correctly outputs the result
https://github.com/dafny-lang/dafny/runs/4797180341?check_suite_focus=true
There is nothing we can test at this stage if this is not a consistent error.

Fix dafny-lang/ide-vscode#131

f834fbc

MikaelMayer requested review from keyboardDrummer and camrein February 14, 2022 21:43

MikaelMayer self-assigned this Feb 14, 2022

MikaelMayer mentioned this pull request Feb 14, 2022

Running JavaScript does not output anything dafny-lang/ide-vscode#131

Closed

MikaelMayer added 2 commits February 14, 2022 16:33

Fixed tests

e5e003c

Better solution less hacky

d002a40

cpitclaudel reviewed Feb 15, 2022

View reviewed changes

camrein reviewed Feb 15, 2022

View reviewed changes

Review comments

69d341e

MikaelMayer requested review from cpitclaudel and camrein February 15, 2022 15:26

camrein previously approved these changes Feb 15, 2022

View reviewed changes

Name of method + Trying to make the tests to pass

c6c9e4f

MikaelMayer dismissed camrein’s stale review via c6c9e4f February 15, 2022 16:17

Simplifying to avoid dealing with lines.

01fdb69

Merge branch 'master' into fix-ide-vscode-131

335007f

MikaelMayer requested a review from camrein February 16, 2022 18:44

cpitclaudel reviewed Feb 16, 2022

View reviewed changes

MikaelMayer added 2 commits February 16, 2022 15:02

Fix the potential deadlock.

6a052ab

Merge branch 'fix-ide-vscode-131' of https://github.com/dafny-lang/dafny

9cbbcae

into fix-ide-vscode-131

cpitclaudel reviewed Feb 16, 2022

View reviewed changes

camrein reviewed Feb 17, 2022

View reviewed changes

camrein requested changes Feb 17, 2022

View reviewed changes

MikaelMayer added 2 commits February 17, 2022 09:30

Review comments

1fd5013

wait on the task that reads the standard error

90c5946

Merge branch 'master' into fix-ide-vscode-131

a8d318c

MikaelMayer requested a review from camrein February 17, 2022 17:00

camrein approved these changes Feb 17, 2022

View reviewed changes

MikaelMayer merged commit 8e753ce into master Feb 17, 2022

MikaelMayer deleted the fix-ide-vscode-131 branch February 17, 2022 20:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix: Output in JavaScript not consistent #1824

Fix: Output in JavaScript not consistent #1824

MikaelMayer commented Feb 14, 2022 •

edited

Loading

cpitclaudel Feb 15, 2022

cpitclaudel Feb 15, 2022

camrein Feb 15, 2022

MikaelMayer Feb 15, 2022

cpitclaudel commented Feb 15, 2022

camrein Feb 15, 2022

camrein Feb 15, 2022

MikaelMayer commented Feb 15, 2022

camrein left a comment

camrein Feb 15, 2022

MikaelMayer Feb 16, 2022

camrein Feb 15, 2022

MikaelMayer commented Feb 16, 2022

cpitclaudel Feb 16, 2022

cpitclaudel Feb 16, 2022

MikaelMayer Feb 16, 2022

cpitclaudel Feb 16, 2022

camrein Feb 17, 2022 •

edited

Loading

MikaelMayer Feb 17, 2022

MikaelMayer Feb 17, 2022

camrein Feb 17, 2022

MikaelMayer Feb 17, 2022

camrein left a comment

camrein left a comment

MikaelMayer commented Feb 17, 2022

Fix: Output in JavaScript not consistent #1824

Fix: Output in JavaScript not consistent #1824

Conversation

MikaelMayer commented Feb 14, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel commented Feb 15, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer commented Feb 15, 2022

camrein left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer commented Feb 16, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

camrein Feb 17, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

camrein left a comment

Choose a reason for hiding this comment

camrein left a comment

Choose a reason for hiding this comment

MikaelMayer commented Feb 17, 2022

MikaelMayer commented Feb 14, 2022 •

edited

Loading

camrein Feb 17, 2022 •

edited

Loading