[isabelle-dev] Jenkins maintenance

[Makarius]

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