On 14/10/2011, at 8:02 PM, Makarius wrote: >> We're investigating if possibly something is wrong with the test server's >> memory, but it seems unlikely (our L4.verified sessions are larger and >> stable). > > Is this the machine that is producing these test results? > > http://isabelle.in.tum.de/devel/stats/afp.html
Yes. > There used to be much less fluctuation with AFP on the hardware at TUM, IIRC. A few years ago, yes, I think. More recently, the test used to crash almost every day at TUM, though, that's why I moved it to this server. The problems at the time seemed file system/NFS related. I have changed the setup since then and made it less dependent on NFS. Maybe it's time to move it back to TUM if we can get a dedicated (for the test time) machine there so we get more reliable timing results. > Since the charts are derived from the "Finished" status it might also involve > the file-system. Instead the inner "Timing" could be used to get closer to > the raw CPU characteristics. Mira should also contain that information. I doubt it's the file system, because there is almost no activity on the file system of that server at all. It doesn't run much else than long Isabelle sessions. The server is nowhere close to saturated in the current configuration, but it's still possible that having another concurrent Isabelle sessions interferes with the runtime. I'd say we keep it with polyml-5.4.1 on that server for another week to find out if the version change fixed that particular problem and then I try moving the test back to a TUM server that doesn't run anything else at the same time. Cheers, Gerwin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
