fix(lsp): kill language server if parent process dies #1664

keyboardDrummer · 2021-12-23T14:14:24Z

…arent dies

…e language server

cpitclaudel · 2021-12-23T14:53:47Z

Source/DafnyLanguageServer/DafnyLanguageServer.cs

+ }
+ catch {
+ // If the process dies before we get here then request shutdown immediately
+ cancelLanguageServer.Cancel();


This will make it harder to test the server independently, because it will prevent us from replaying previously-recorded LSP traces. Can we find a trick to have the server ignore this in some cases? Maybe it's enough to do nothing in this catch case?

Would it be possible to change the ParentId in the Initialize request when replaying the messages?

Yes, certainly.

cpitclaudel · 2021-12-23T14:54:11Z

Source/DafnyLanguageServer/Program.cs

 );
+ cancelLanguageServer.Token.Register(() => server.ForcefulShutdown());


I think it would be good to log something here.

Added a log message, although in another location

…eath

Source/DafnyLanguageServer.Test/Various/StartLanguageServer.cs

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

MikaelMayer · 2021-12-23T15:27:39Z

Source/DafnyLanguageServer/DafnyLanguageServer.cs

 var logger = server.GetRequiredService<ILogger<Program>>();
 logger.LogTrace("initializing service");
+
+ KillLanguageServerIfParentDies(request, cancelLanguageServer);


I'm very new to this code, so I need to better understand it.
Why was the request not used before? Is this code run for every request?

The request is also used in another location, but this method allows you do additional work. An InitializeParams request is sent at most once, so this code is run at most once.

cpitclaudel · 2021-12-23T16:29:01Z

This implementation strategy looks good to me. I'm surprised that the VSCode folks don't clean up language server processes when the IDE is killed.

keyboardDrummer · 2021-12-23T17:14:52Z

This implementation strategy looks good to me. I'm surprised that the VSCode folks don't clean up language server processes when the IDE is killed.

The LSP server process is not started by VSCode but by the LSP client NPM package that the Dafny extension uses, but that's a Microsoft package so you might be just as surprised :D

There's different ways of connecting to a language server with that client though, not all of them start a fresh language server.

Source/DafnyLanguageServer/DafnyLanguageServer.cs

cpitclaudel · 2021-12-23T17:19:33Z

Source/DafnyLanguageServer/DafnyLanguageServer.cs

+ var hostProcess = Process.GetProcessById((int)request.ProcessId)!;
+ hostProcess.EnableRaisingEvents = true;
+ hostProcess.Exited += (_, _) => Kill();
+ } catch {


Can we catch a more specific exception? And maybe shrink the try block to just the GetProcessById?

Catching ArgumentException now. Do you feel the shrinking is worth the extra verbosity?

Yes, but in fact camrein suggested an even better alternative (an explicit assertion)

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

cpitclaudel · 2021-12-23T17:27:24Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

+ var error = "";
+ process.ErrorDataReceived += delegate (object sender, DataReceivedEventArgs args) { error += args.Data; };
+
+ var languageServerProcessId = await process.StandardOutput.ReadLineAsync();


Why do you wrap a custom binary that prints its PID around the server instead of just reading the PID of the regular server?

We need to pass the PID of a running process to the language server in the initialize request, and later kill that process. This is what the custom binary is for. It also starts the language server to make the test more realistic, since the PID is supposed to be the parent process of the language server.

Then I think your solution makes sense, thanks!

cpitclaudel

LGTM, but I'm a bit confused by the testing strategy (I don't see yet why we need a custom binary to wrap the server).

camrein · 2021-12-24T12:32:59Z

Source/DafnyLanguageServer/DafnyLanguageServer.cs

 .OnStarted(StartedAsync);
 }

- private static Task InitializeAsync(ILanguageServer server, InitializeParams request, CancellationToken cancellationToken) {
+ private static Task InitializeAsync(ILanguageServer server, InitializeParams request, CancellationToken cancelRequestToken,
+ CancellationTokenSource cancelLanguageServer) {
 var logger = server.GetRequiredService<ILogger<Program>>();


That's something I must have missed when I extracted the WithDafnyLanguageServer method into a separate class. Could you change the injected logger instance to ILogger<DafnyLanguageServer>?

camrein · 2021-12-24T13:36:01Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

@@ -24,24 +24,23 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various {
 [TestClass]
 public class ShutdownTest {

- [TestMethod]
+ [TestMethod, Timeout(10000)]


For readability, you may want to write the literal as 10_000.

camrein · 2021-12-24T13:38:40Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

- MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location),
- MetadataReference.CreateFromFile(Assembly.Load("mscorlib").Location));
+ MetadataReference.CreateFromFile(Assembly.Load(fileName).Location))).
+ AddReferences(


So far I applied the convention to use the dot of method chained calls as a prefix.

camrein · 2021-12-24T13:39:26Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

+  AddReferences(
+  MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location),
+  MetadataReference.CreateFromFile(Assembly.Load("mscorlib").Location));
+ compilation = compilation.WithOptions(new CSharpCompilationOptions(OutputKind.ConsoleApplication));


You could continue the method chaining here since you neither explicitly name nor use the intermediate state.

camrein

Looks good so far. I've added two more comments to the others.

PS: We may switch to XUnit in the future since the rest of Dafny's test suite is built around it.

camrein · 2021-12-27T07:32:41Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

+ languageServer.Kill();
+ Assert.Fail("Language server should have killed itself if the parent is gone.");
+ } catch (ArgumentException) {
+ // Language server process is not running, pass the test.


There's a suitable assertion in MSTest:

Assert.ThrowsException<ArgumentException>(() => { var languageServer = Process.GetProcessById(int.Parse(languageServerProcessId)); languageServer.Kill(); });

Source/DafnyLanguageServer/DafnyLanguageServer.cs

…r/dafny into issue95RunawayZ3Processes

MikaelMayer

Well done for this one.
Next one interesting to solve would be the memory leak of a single DafnyLanguageServer with "save on change" that keeps too much in memory and goes to 4Gb of RAM in a few minutes.

Source/DafnyLanguageServer/DafnyLanguageServer.cs

MikaelMayer · 2021-12-27T16:45:16Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

+using System.Diagnostics;
+using System.Threading.Tasks;
+
+public class ShortLivedProcessStarter {{


I like this name.

camrein

Thanks for the improvements. Since I belive the use of CancellationTokenSource is now unnecessary, I've requested one more change. After that, we're good to go.

Source/DafnyLanguageServer/DafnyLanguageServer.cs

camrein · 2021-12-28T09:24:01Z

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs

+ }
+ });
+#pragma warning disable VSTHRD002
+ outputHandler.StopAsync().Wait();


Any reason for this? I see that the target buffer is a MemoryStream; thus, the actions tend to be synchronous anyway. However, it would make the warning suppression obsolete, as well as the use of Wait that would require manual unwrapping of the nested exceptions.

Source/DafnyLanguageServer/Program.cs

keyboardDrummer requested review from fabiomadge, MikaelMayer, camrein and atomb December 23, 2021 14:14

Remy Willems added 8 commits December 23, 2021 15:50

Create test for checking if the language server kills itself if the p…

678892b

…arent dies

Tests pasS

e695a26

Test improvements

72fb5fc

Improve test by not killing the parent process before initializing th…

6846642

…e language server

Ran formatter

9b10e98

Refactor code

4d7be31

Rename

9c6c48e

Formatting

7d6293b

cpitclaudel reviewed Dec 23, 2021

View reviewed changes

Fix tests

53faa7a

keyboardDrummer force-pushed the issue95RunawayZ3Processes branch from ab4e0e1 to 53faa7a Compare December 23, 2021 15:03

Log warning when language server kills itself due to parent process d…

96acbe2

…eath

MikaelMayer reviewed Dec 23, 2021

View reviewed changes

keyboardDrummer requested a review from cpitclaudel December 23, 2021 17:15

cpitclaudel reviewed Dec 23, 2021

View reviewed changes

Source/DafnyLanguageServer/DafnyLanguageServer.cs Show resolved Hide resolved

Fix bug

30e8ec7

cpitclaudel reviewed Dec 23, 2021

View reviewed changes

Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs Show resolved Hide resolved

cpitclaudel reviewed Dec 23, 2021

View reviewed changes

Remy Willems added 2 commits December 23, 2021 18:50

Add fix for windows and increase sleep

9cfc07c

Catching more specific exception

224b875

keyboardDrummer requested a review from MikaelMayer December 23, 2021 18:06

keyboardDrummer requested a review from camrein December 24, 2021 11:22

camrein reviewed Dec 24, 2021

View reviewed changes

Remy Willems added 2 commits December 24, 2021 15:47

Small refactoring

e360fc5

Fix oops

7e207d1

keyboardDrummer force-pushed the issue95RunawayZ3Processes branch from 1d0efcf to 7e207d1 Compare December 24, 2021 14:49

keyboardDrummer requested a review from camrein December 24, 2021 14:49

camrein reviewed Dec 27, 2021

View reviewed changes

Remy Willems and others added 2 commits December 27, 2021 11:22

Use Assert.ThrowsException

6055621

Merge branch 'master' into issue95RunawayZ3Processes

1538c42

keyboardDrummer requested a review from camrein December 27, 2021 10:22

keyboardDrummer and others added 2 commits December 27, 2021 11:39

Merge branch 'master' into issue95RunawayZ3Processes

bd739be

Merge branch 'issue95RunawayZ3Processes' of github.com:keyboardDrumme…

ce67189

…r/dafny into issue95RunawayZ3Processes

fabiomadge previously approved these changes Dec 27, 2021

View reviewed changes

MikaelMayer previously approved these changes Dec 27, 2021

View reviewed changes

camrein requested changes Dec 28, 2021

View reviewed changes

Refactoring

55dae8e

keyboardDrummer dismissed stale reviews from MikaelMayer and fabiomadge via 55dae8e December 28, 2021 10:16

Merge branch 'master' into issue95RunawayZ3Processes

34ef4a0

keyboardDrummer requested a review from camrein December 28, 2021 10:19

Merge branch 'master' into issue95RunawayZ3Processes

1fb01ab

cpitclaudel approved these changes Dec 28, 2021

View reviewed changes

camrein approved these changes Dec 28, 2021

View reviewed changes

Merge branch 'master' into issue95RunawayZ3Processes

68e4c16

keyboardDrummer enabled auto-merge (squash) December 28, 2021 16:49

keyboardDrummer merged commit b3254b4 into dafny-lang:master Dec 28, 2021

keyboardDrummer deleted the issue95RunawayZ3Processes branch December 28, 2021 17:13

This was referenced Jan 4, 2022

Language Server verifying forever and/or leaving orphaned dotnet/z3 processes #1611

Closed

Feature request: language server: terminate running Z3s when client disconnects #1690

Closed

This pull request was closed.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix(lsp): kill language server if parent process dies #1664

fix(lsp): kill language server if parent process dies #1664

keyboardDrummer commented Dec 23, 2021

cpitclaudel Dec 23, 2021

keyboardDrummer Dec 23, 2021

cpitclaudel Dec 23, 2021

cpitclaudel Dec 23, 2021

keyboardDrummer Dec 23, 2021

MikaelMayer Dec 23, 2021

keyboardDrummer Dec 23, 2021

cpitclaudel commented Dec 23, 2021

keyboardDrummer commented Dec 23, 2021 •

edited

Loading

cpitclaudel Dec 23, 2021

keyboardDrummer Dec 23, 2021

cpitclaudel Dec 28, 2021

cpitclaudel Dec 23, 2021

keyboardDrummer Dec 23, 2021

cpitclaudel Dec 28, 2021

cpitclaudel left a comment

camrein Dec 24, 2021

camrein Dec 24, 2021

camrein Dec 24, 2021

camrein Dec 24, 2021

camrein left a comment

camrein Dec 27, 2021

MikaelMayer left a comment •

edited

Loading

MikaelMayer Dec 27, 2021

camrein left a comment

camrein Dec 28, 2021

		);
		cancelLanguageServer.Token.Register(() => server.ForcefulShutdown());

fix(lsp): kill language server if parent process dies #1664

fix(lsp): kill language server if parent process dies #1664

Conversation

keyboardDrummer commented Dec 23, 2021

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel commented Dec 23, 2021

keyboardDrummer commented Dec 23, 2021 • 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

Choose a reason for hiding this comment

cpitclaudel 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

Choose a reason for hiding this comment

camrein left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment • edited Loading

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

Choose a reason for hiding this comment

keyboardDrummer commented Dec 23, 2021 •

edited

Loading

MikaelMayer left a comment •

edited

Loading