Indeed, regardless of the multiplier, I never see more than around 20
alt-ergo processes running, even though I asked for 40. So I guess that
most of the time is used on generating the verification conditions.
julia
___
Why3-club mailing list
Why3-club@
Yes, please do.
On Sat, 20 Apr 2019 at 12:37, Julia Lawall wrote:
>
>
> On Sat, 20 Apr 2019, Andrei Paskevich wrote:
>
> > Sorry, I meant each 0.1 sec, of course.
> >
> > The 3x factor is, if I remember correctly, the upper bound on the backlog
> > size: Why3 stops preparing tasks once it has 3x
On Sat, 20 Apr 2019, Andrei Paskevich wrote:
> Sorry, I meant each 0.1 sec, of course.
>
> The 3x factor is, if I remember correctly, the upper bound on the backlog
> size: Why3 stops preparing tasks once it has 3x#cores tasks ready to go. I
> don't think lowering it is a good solution long-term
Sorry, I meant each 0.1 sec, of course.
The 3x factor is, if I remember correctly, the upper bound on the backlog
size: Why3 stops preparing tasks once it has 3x#cores tasks ready to go. I
don't think lowering it is a good solution long-term: what we probably
should do is to schedule interruptions
On Sat, 20 Apr 2019, Andrei Paskevich wrote:
> Indeed, with as many as 47 cores ready to run external provers, Why3 is sure
> busy to fill the working queue with prepared proof tasks. I am not sure what
> is the right approach here: set some real-time bounds and go back to UI,
> say, each tenth
Indeed, with as many as 47 cores ready to run external provers, Why3 is
sure busy to fill the working queue with prepared proof tasks. I am not
sure what is the right approach here: set some real-time bounds and go back
to UI, say, each tenth second, even if the backlog is still being filled?
A.
_
Le 20/04/2019 à 11:29, Julia Lawall a écrit :
Keep in mind that Why3 is inherently mono-core. So, Why3 will be
unusable until the 10 corresponding proof obligations have been
generated and sent to external provers.
More generally, the more cores you computer has, the more proof
obligations Why3
On Sat, 20 Apr 2019, Guillaume Melquiond wrote:
> Le 19/04/2019 à 13:41, Julia Lawall a écrit :
>
> >> I'm not sure how to help, but I wonder: how many provers you asked Why3
> >> to run in parallel? I suggest you should not use 48, because you will
> >> have no remaining cores for the main Why3
On Sat, 20 Apr 2019, Guillaume Melquiond wrote:
> Le 19/04/2019 à 13:41, Julia Lawall a écrit :
>
> >> I'm not sure how to help, but I wonder: how many provers you asked Why3
> >> to run in parallel? I suggest you should not use 48, because you will
> >> have no remaining cores for the main Why3
Le 19/04/2019 à 13:41, Julia Lawall a écrit :
I'm not sure how to help, but I wonder: how many provers you asked Why3
to run in parallel? I suggest you should not use 48, because you will
have no remaining cores for the main Why3 process, and other processes
of your system.
I asked for 47.
Bu
On Fri, 19 Apr 2019, Claude Marche wrote:
>
> Hello Julia,
>
> I'm not sure how to help, but I wonder: how many provers you asked Why3
> to run in parallel? I suggest you should not use 48, because you will
> have no remaining cores for the main Why3 process, and other processes
> of your system
Hello Julia,
I'm not sure how to help, but I wonder: how many provers you asked Why3
to run in parallel? I suggest you should not use 48, because you will
have no remaining cores for the main Why3 process, and other processes
of your system.
- Claude
Le 18/04/2019 à 11:35, Julia Lawall a é
Hello,
I wonder if there is a concurrency problem that could be easily solved? I
use why3 on a 48 core server. When I start up why3, when I refresh, or
run obsolete proofs, there is a long time (maybe one minute) where the ide
is not responsive. When I use top, I see the solvers running. But i
13 matches
Mail list logo
