On 06/10/16 15:07, Lars Hupel wrote: > In fact, the situation was even worse back then: Various Isabelle > developers have told me that they're using "macbroy2" which would > otherwise be used for isatest/afptest for private experiments. Since a > full test run would sometimes take some 10 hours, collisions were pretty > much guaranteed. > > There cannot be useful performance measurements unless the environment > is controlled, i.e. free of other accesses.
The general policies are rather simple: * automated tests are run during the night * humans use the same hardware during the day * everybody understands the difference, and takes care to avoid conflicts For the new hardware, it could be done slightly differently: * CPU 0 is exclusive for automated tests * CPU 1 is exclusive for manual tests >From the hardware architecture, such a clear separation of the two CPU sockets with their local memory modules could work, but it requires proper physical experiments prove that. Splitting a single CPU socket into logical parts (as done now) is likely to cause conflicts via caches. It might be one of the reasons, why the current Jenkins measurements are still quite erratic. Moreover, enabling hyperthreading on the CPU for manual testing would give another factor of 1.2. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev