Re: [Why3-club] Running multiple provers in parallel on a single task

[Claude Marché]

Le 23/10/2017 à 13:59, Pierre-Yves Strub a écrit :
> Hi again,
> 
> If found Call_prover.forward_results in the git repository and this is
> definitively what I need. This new API is great as it will allow
> EasyCrypt to run multiple provers in parallel under Windows
> (currently, we are running provers one by one under win32) & will
> allow me to remove all this fork/waitpid stuffs in our code base. I
> have a few questions/requests :
> 
>   - when do you plan to release Why3 with "forward_results" available
> --- if I'm right, it is not present in Why3 0.88.0?

Ouch, sorry, I though it was already there in Why3 0.88.0

The current master branch of the git contains a lot of diffs with 0.88,
regarding the structure of sessions, and the GTK interface. Since you
are not using them, then master branch could be suitable for you.

However, I guess you would like to rely on a Why3 release, available
e.g. in OPAM ?

Then indeed, we might need to make a 0.88.1 release soon. We'll try to
do our best to make one.

>   - I need to create search trees or hash tables using job IDs as key,
> i.e. using prover_call as key. Currently, breaking the abstraction, I
> can see that using the polymorphic comparison/hash functions, all will
> be fine... but having explicit eq/compare/hash functions for the
> prover_call type would allow me not to rely on breaking the Why3 API
> abstraction.

Good point, we should add them in the API.

- Claude


-- 
Claude Marché  | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France   |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Running multiple provers in parallel on a single task

[Pierre-Yves Strub]

Last thing, when a prover returns that a task is valid, I'd like to be
able to kill the other ones (I was doing this with a kill(2) syscall
before). Would it be possible to have such a thing with a function
using call_prover as argument?

2017-10-23 13:59 GMT+02:00 Pierre-Yves Strub :
> Hi again,
>
> If found Call_prover.forward_results in the git repository and this is
> definitively what I need. This new API is great as it will allow
> EasyCrypt to run multiple provers in parallel under Windows
> (currently, we are running provers one by one under win32) & will
> allow me to remove all this fork/waitpid stuffs in our code base. I
> have a few questions/requests :
>
>   - when do you plan to release Why3 with "forward_results" available
> --- if I'm right, it is not present in Why3 0.88.0?
>   - I need to create search trees or hash tables using job IDs as key,
> i.e. using prover_call as key. Currently, breaking the abstraction, I
> can see that using the polymorphic comparison/hash functions, all will
> be fine... but having explicit eq/compare/hash functions for the
> prover_call type would allow me not to rely on breaking the Why3 API
> abstraction.
>
> Best. Pierre-Yves.
>
>
> 2017-10-23 13:36 GMT+02:00 Claude Marché :
>>
>> Hello,
>>
>> Indeed, the API from Call_provers.mli has changed (yet another
>> not-well-documented Why3 change, sorry about that)
>>
>> For sure the use of Why3 "strategies" is not what you need.
>>
>> The main change is that for spawning provers as external processes, Why3
>> does not anymore proceed using a fork, but instead delegates this to
>> another process so-called "why3server". This approach solved at least
>> two issues: first, it is now compatible with Microsoft Windows OS, and
>> second the size of the forked processes is considerably smaller.
>>
>> From the Why3's user side, there is no visible change, except if you are
>> an advanced user using the API directly.
>>
>> It seems to me that, as suggested by Johannes, the use of the
>> prover_call type should abstract away the unix pid. Regarding your
>> request of having a way to call for available answers from multiple
>> provers, the function
>>
>> Call_prover.forward_results
>>
>> should be what you look for.
>>
>> If something is missing for you in this API, we would be glad to
>> complete it for your need.
>>
>> - Claude
>>
>> Le 23/10/2017 à 13:12, Pierre-Yves Strub a écrit :
>>> Thank you for your answer. Yes, I was speaking about process ID that
>>> were available up to Why 0.87. We're not using sessions and
>>> Driver.prove_task which returns a Call_provers.prover_call (as the
>>> call_on_*). The problem is that with the new API, I don't have any way
>>> to wait for multiple provers (in a non-active way, i.e. without
>>> spamming query_call). I'm ok to move to any API as long as I can call
>>> multiple provers on a task and wait until on prover succeeds.
>>>
>>> Best. Pierre-Yves.
>>>
>>> 2017-10-23 11:47 GMT+02:00 Johannes Kanig :
 Dear Pierre-Yves,

 On 10/23/2017 06:27 PM, Pierre-Yves Strub wrote:
>
> I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we
> were using the Why3 API to run provers on a task that we create
> programmatically. To start multiple provers in parallel, we were
> running our home made machinery that was relying on PID.


 are you referring to the process ID? Indeed, why3 doesn't necessarily spawn
 the prover process itself, so doesn't necessarily have access to the pid.

> This API has
> now been removed (if I understand well because running a prover does
> not necessarily mean forking a new process in Why3 0.88).


>  From the API documentation, it seems that I could now achieve the same
> thing using the Strategy API. However, I failed understanding how the
> API works. Could someone give me some pointers to which
> modules/functions I should look at?


 Were you previously using sessions? If not, you can just replace your pids
 by the "prover_call" type of call_provers.mli. The call_on_* functions of
 that file (and the more high-level ones of driver.mli) return immediately,
 so they are suitable for running provers in parallel.

 --
 Johannes Kanig, PhD
 Senior Software Engineer
 >> ___
>>> Why3-club mailing list
>>> Why3-club@lists.gforge.inria.fr
>>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>>>
>>
>> --
>> Claude Marché  | tel: +33 1 69 15 66 08
>> INRIA Saclay - Île-de-France   |
>> Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
>> F-91405 ORSAY Cedex

Re: [Why3-club] Running multiple provers in parallel on a single task

[Pierre-Yves Strub]

Hi again,

If found Call_prover.forward_results in the git repository and this is
definitively what I need. This new API is great as it will allow
EasyCrypt to run multiple provers in parallel under Windows
(currently, we are running provers one by one under win32) & will
allow me to remove all this fork/waitpid stuffs in our code base. I
have a few questions/requests :

  - when do you plan to release Why3 with "forward_results" available
--- if I'm right, it is not present in Why3 0.88.0?
  - I need to create search trees or hash tables using job IDs as key,
i.e. using prover_call as key. Currently, breaking the abstraction, I
can see that using the polymorphic comparison/hash functions, all will
be fine... but having explicit eq/compare/hash functions for the
prover_call type would allow me not to rely on breaking the Why3 API
abstraction.

Best. Pierre-Yves.


2017-10-23 13:36 GMT+02:00 Claude Marché :
>
> Hello,
>
> Indeed, the API from Call_provers.mli has changed (yet another
> not-well-documented Why3 change, sorry about that)
>
> For sure the use of Why3 "strategies" is not what you need.
>
> The main change is that for spawning provers as external processes, Why3
> does not anymore proceed using a fork, but instead delegates this to
> another process so-called "why3server". This approach solved at least
> two issues: first, it is now compatible with Microsoft Windows OS, and
> second the size of the forked processes is considerably smaller.
>
> From the Why3's user side, there is no visible change, except if you are
> an advanced user using the API directly.
>
> It seems to me that, as suggested by Johannes, the use of the
> prover_call type should abstract away the unix pid. Regarding your
> request of having a way to call for available answers from multiple
> provers, the function
>
> Call_prover.forward_results
>
> should be what you look for.
>
> If something is missing for you in this API, we would be glad to
> complete it for your need.
>
> - Claude
>
> Le 23/10/2017 à 13:12, Pierre-Yves Strub a écrit :
>> Thank you for your answer. Yes, I was speaking about process ID that
>> were available up to Why 0.87. We're not using sessions and
>> Driver.prove_task which returns a Call_provers.prover_call (as the
>> call_on_*). The problem is that with the new API, I don't have any way
>> to wait for multiple provers (in a non-active way, i.e. without
>> spamming query_call). I'm ok to move to any API as long as I can call
>> multiple provers on a task and wait until on prover succeeds.
>>
>> Best. Pierre-Yves.
>>
>> 2017-10-23 11:47 GMT+02:00 Johannes Kanig :
>>> Dear Pierre-Yves,
>>>
>>> On 10/23/2017 06:27 PM, Pierre-Yves Strub wrote:

 I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we
 were using the Why3 API to run provers on a task that we create
 programmatically. To start multiple provers in parallel, we were
 running our home made machinery that was relying on PID.
>>>
>>>
>>> are you referring to the process ID? Indeed, why3 doesn't necessarily spawn
>>> the prover process itself, so doesn't necessarily have access to the pid.
>>>
 This API has
 now been removed (if I understand well because running a prover does
 not necessarily mean forking a new process in Why3 0.88).
>>>
>>>
  From the API documentation, it seems that I could now achieve the same
 thing using the Strategy API. However, I failed understanding how the
 API works. Could someone give me some pointers to which
 modules/functions I should look at?
>>>
>>>
>>> Were you previously using sessions? If not, you can just replace your pids
>>> by the "prover_call" type of call_provers.mli. The call_on_* functions of
>>> that file (and the more high-level ones of driver.mli) return immediately,
>>> so they are suitable for running provers in parallel.
>>>
>>> --
>>> Johannes Kanig, PhD
>>> Senior Software Engineer
>>> >> ___
>>> Why3-club mailing list
>>> Why3-club@lists.gforge.inria.fr
>>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>> ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>>
>
> --
> Claude Marché  | tel: +33 1 69 15 66 08
> INRIA Saclay - Île-de-France   |
> Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex|
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Running multiple provers in parallel on a single task

[Claude Marché]

Hello,

Indeed, the API from Call_provers.mli has changed (yet another
not-well-documented Why3 change, sorry about that)

For sure the use of Why3 "strategies" is not what you need.

The main change is that for spawning provers as external processes, Why3
does not anymore proceed using a fork, but instead delegates this to
another process so-called "why3server". This approach solved at least
two issues: first, it is now compatible with Microsoft Windows OS, and
second the size of the forked processes is considerably smaller.

From the Why3's user side, there is no visible change, except if you are
an advanced user using the API directly.

It seems to me that, as suggested by Johannes, the use of the
prover_call type should abstract away the unix pid. Regarding your
request of having a way to call for available answers from multiple
provers, the function

Call_prover.forward_results

should be what you look for.

If something is missing for you in this API, we would be glad to
complete it for your need.

- Claude

Le 23/10/2017 à 13:12, Pierre-Yves Strub a écrit :
> Thank you for your answer. Yes, I was speaking about process ID that
> were available up to Why 0.87. We're not using sessions and
> Driver.prove_task which returns a Call_provers.prover_call (as the
> call_on_*). The problem is that with the new API, I don't have any way
> to wait for multiple provers (in a non-active way, i.e. without
> spamming query_call). I'm ok to move to any API as long as I can call
> multiple provers on a task and wait until on prover succeeds.
> 
> Best. Pierre-Yves.
> 
> 2017-10-23 11:47 GMT+02:00 Johannes Kanig :
>> Dear Pierre-Yves,
>>
>> On 10/23/2017 06:27 PM, Pierre-Yves Strub wrote:
>>>
>>> I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we
>>> were using the Why3 API to run provers on a task that we create
>>> programmatically. To start multiple provers in parallel, we were
>>> running our home made machinery that was relying on PID.
>>
>>
>> are you referring to the process ID? Indeed, why3 doesn't necessarily spawn
>> the prover process itself, so doesn't necessarily have access to the pid.
>>
>>> This API has
>>> now been removed (if I understand well because running a prover does
>>> not necessarily mean forking a new process in Why3 0.88).
>>
>>
>>>  From the API documentation, it seems that I could now achieve the same
>>> thing using the Strategy API. However, I failed understanding how the
>>> API works. Could someone give me some pointers to which
>>> modules/functions I should look at?
>>
>>
>> Were you previously using sessions? If not, you can just replace your pids
>> by the "prover_call" type of call_provers.mli. The call_on_* functions of
>> that file (and the more high-level ones of driver.mli) return immediately,
>> so they are suitable for running provers in parallel.
>>
>> --
>> Johannes Kanig, PhD
>> Senior Software Engineer
>> > ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 

-- 
Claude Marché  | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France   |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Running multiple provers in parallel on a single task

[Pierre-Yves Strub]

Sorry, my sentence is unclear: We're not using sessions but are
already using Driver.prove_task which returns a
Call_provers.prover_call (as the
call_on_*).

2017-10-23 13:12 GMT+02:00 Pierre-Yves Strub :
> Thank you for your answer. Yes, I was speaking about process ID that
> were available up to Why 0.87. We're not using sessions and
> Driver.prove_task which returns a Call_provers.prover_call (as the
> call_on_*). The problem is that with the new API, I don't have any way
> to wait for multiple provers (in a non-active way, i.e. without
> spamming query_call). I'm ok to move to any API as long as I can call
> multiple provers on a task and wait until on prover succeeds.
>
> Best. Pierre-Yves.
>
> 2017-10-23 11:47 GMT+02:00 Johannes Kanig :
>> Dear Pierre-Yves,
>>
>> On 10/23/2017 06:27 PM, Pierre-Yves Strub wrote:
>>>
>>> I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we
>>> were using the Why3 API to run provers on a task that we create
>>> programmatically. To start multiple provers in parallel, we were
>>> running our home made machinery that was relying on PID.
>>
>>
>> are you referring to the process ID? Indeed, why3 doesn't necessarily spawn
>> the prover process itself, so doesn't necessarily have access to the pid.
>>
>>> This API has
>>> now been removed (if I understand well because running a prover does
>>> not necessarily mean forking a new process in Why3 0.88).
>>
>>
>>>  From the API documentation, it seems that I could now achieve the same
>>> thing using the Strategy API. However, I failed understanding how the
>>> API works. Could someone give me some pointers to which
>>> modules/functions I should look at?
>>
>>
>> Were you previously using sessions? If not, you can just replace your pids
>> by the "prover_call" type of call_provers.mli. The call_on_* functions of
>> that file (and the more high-level ones of driver.mli) return immediately,
>> so they are suitable for running provers in parallel.
>>
>> --
>> Johannes Kanig, PhD
>> Senior Software Engineer
>> > ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Running multiple provers in parallel on a single task

[Johannes Kanig]

Dear Pierre-Yves,

On 10/23/2017 06:27 PM, Pierre-Yves Strub wrote:

I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we
were using the Why3 API to run provers on a task that we create
programmatically. To start multiple provers in parallel, we were
running our home made machinery that was relying on PID.


are you referring to the process ID? Indeed, why3 doesn't necessarily 
spawn the prover process itself, so doesn't necessarily have access to 
the pid.



This API has
now been removed (if I understand well because running a prover does
not necessarily mean forking a new process in Why3 0.88).



 From the API documentation, it seems that I could now achieve the same
thing using the Strategy API. However, I failed understanding how the
API works. Could someone give me some pointers to which
modules/functions I should look at?


Were you previously using sessions? If not, you can just replace your 
pids by the "prover_call" type of call_provers.mli. The call_on_* 
functions of that file (and the more high-level ones of driver.mli) 
return immediately, so they are suitable for running provers in parallel.


--
Johannes Kanig, PhD
Senior Software Engineer