search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Travis CI failing nondeterministically #279

Closed zvonimir closed 6 years ago

zvonimir commented 7 years ago

The issue seems to be that the C# compiler (csc binary) occasionally hangs. I observed the same problem with vagrant sometimes. I have no idea what is causing this or how I would go about fixing it. I am kind of hoping it'll fix itself on its own.

michael-emmi commented 6 years ago

Do you have a demonstration (trace) of this?

How sure are you that it is hanging, versus working but not producing output for a while?

I recently learned that builds can time out when there’s no output for some time; and Travis provides a way to subvert this.

https://docs.travis-ci.com/user/common-build-problems/#Build-times-out-because-no-output-was-received

zvonimir commented 6 years ago

Well, I observe this same behavior sometimes with vagrant as well. I just hangs when compiling a file. I waited for a while (think 20 mins) and nothing happened. So I think it somehow hangs. What do you mean by "trace"? I could see the exact compiler invocation that hangs will all the arguments. So I could maybe copy-paste that here. The weird part is that it does not hang always, but only occasionally. Maybe once every 10 builds or something like that.

zvonimir commented 6 years ago

Ok, I just encountered this issue on a local Ubuntu machine. Here is where it hangs (I've been waiting for 10 minutes and no obvious progress has been made):

Done Building Project "/uusoc/exports/scratch/rise4fun/corral/boogie/Source/Concurrency/Concurrency.csproj" (default targets).
Project "/uusoc/exports/scratch/rise4fun/corral/cba.csproj" (2) is building "/uusoc/exports/scratch/rise4fun/corral/boogie/Source/ExecutionEngine/ExecutionEngine.csproj" (8:2) on node 1 (default targets).
PrepareForBuild:
  Creating directory "obj/Release/".
Project "/uusoc/exports/scratch/rise4fun/corral/boogie/Source/ExecutionEngine/ExecutionEngine.csproj" (8:2) is building "/uusoc/exports/scratch/rise4fun/corral/boogie/Source/Doomed/Doomed.csproj" (20:2) on node 1 (default targets).
PrepareForBuild:
  Creating directory "bin/Release/".
  Creating directory "obj/Release/".
Project "/uusoc/exports/scratch/rise4fun/corral/boogie/Source/Doomed/Doomed.csproj" (20:2) is building "/uusoc/exports/scratch/rise4fun/corral/boogie/Source/Model/Model.csproj" (11:4) on node 1 (default targets).
PrepareForBuild:
  Creating directory "obj/Release/".
GenerateTargetFrameworkMonikerAttribute:
Skipping target "GenerateTargetFrameworkMonikerAttribute" because all output files are up-to-date with respect to the input files.
CoreCompile:
  /usr/lib/mono/4.5/csc.exe /noconfig /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:TRACE /highentropyva+ /reference:/usr/lib/mono/4.5-api/mscorlib.dll /reference:/usr/lib/mono/4.5-api/System.Core.dll /reference:/usr/lib/mono/4.5-api/System.dll /debug:pdbonly /filealign:512 /keyfile:../InterimKey.snk /optimize+ /out:obj/Release/BoogieModel.dll /subsystemversion:6.00 /target:library /utf8output /publicsign+ Model.cs ModelParser.cs Properties/AssemblyInfo.cs ../version.cs "/tmp/.NETFramework,Version=v4.5.AssemblyAttributes.cs"
michael-emmi commented 6 years ago

That is odd. I wonder whether we can pin this on some recent change?

Since you reproduce this locally, I guess we can rule out Travis.

Any idea whether the Mono package could have changed recently?

Otherwise, I guess it should be some Mono bug that is exposed with some recent version of Corral or Boogie. Have we updated Corral or Boogie recently?

zvonimir commented 6 years ago

Well, it seems to be happening on a random C# file - it seems to be a different file every time I believe. Hence, my hunch is that it is because of a bug in Mono, which updates pretty regularly. One thing we could do it to try and fix Mono version on our end. Or hopefully they'll fix it soon on their end.

zvonimir commented 6 years ago

I just looked at the mono project webpage, and it seems their next release will come out pretty soon (in the next month or so). So I suggest we just wait and see if this problem goes away with the new release.

michael-emmi commented 6 years ago

Another idea: perhaps this might be a good time to switch to Microsoft’s own C# compiler?

michael-emmi commented 6 years ago

Another idea: Travis CI build caching? not sure how this works but maybe we can cache a stable build of dependencies, and then just build Smack after loading the build of dependencies from the cache?

zvonimir commented 6 years ago

After reading a bunch over the weekend, my hunch is that in the long run this is what should be done: https://github.com/boogie-org/boogie/issues/81 I attempted this switch by doing 2-3 obvious updates, but I got stuck with various compilation errors related to framework versions and such. I will get back to this in a day or two. Yeah, Travis caching might be another patch to try out.