[SMT-COMP] dual-core for SMT-COMP 2010?

[Aaron Stump]

Hi, everyone.

Thanks for the feedback, Ken, Johannes, and Roberto.  It seems a very
reasonable suggestion that if we want to enable dual-core, we do so somehow
for a separate category of the competition.  We (the 2010 organizers) will
discuss this internally to see if there is a sensible way to do that.

Happy New Year to all,
Aaron

On Tue, Jan 5, 2010 at 10:37 AM, Roberto Sebastiani <rseba at disi.unitn.it>wrote:

> Aaron,
> sorry for the late reply.
>
>
> If the idea is to allow dual core for all the competition, let me say that
> I'm strongly against it. In fact, the empirical results would completely be
> biased by the usage of the dual core, and the competition may reduce most to
> engineering issues to support concurrency on a specific architecture. Even
> if this were not the case, it would be nearly impossible to decouple the
> advantages of novel techniques and algorithms to those of dual-core support.
>
> If the proposal is instead to make one or more special categories in which
> dual-core can be expoited, I think this could be a nice experiment.
>
> Roberto
>
> -------------------------------------------------------------------------
> Prof. ROBERTO SEBASTIANI
> Dip. Ingegneria e Scienza dell'Informazione, DISI    Tel: +39 0461 881514
> Fac. Scienze M.F.N., Universita` di Trento           Fax: +39 0461 883964
> Via Sommarive 14, I-38123, Povo, Trento, Italy Skype: roberto.sebastiani1
> email: roberto.sebastiani at disi.unitn.it  url: http://disi.unitn.it/~rseba
> OKKAM id: http://www.okkam.org/ens/id4e14c363-3008-4752-b243-480c87eb2b4c
> -------------------------------------------------------------------------
>
>
> On Thu, 31 Dec 2009, Aaron Stump wrote:
>
>  Dear SMT-COMP community,
>>
>> I'm writing to ask your opinion about whether or not we should enable the
>> dual-core feature of our cluster (www.smtexec.org) for SMT-COMP 2010. The
>> cluster machines all have dual cores, but we have disabled the use of the
>> second core in all previous competitions. The motivation for enabling it,
>> of
>> course, is to incentivize solver implementors to add some support for
>> concurrency to their tools. This could lead to significant benefits for
>> the
>> applications that use SMT solvers. As the SMT field has matured over the
>> past five years or so, it seems time to take this next step, to encourage
>> and reward concurrent implementations. This does, of course, impose an
>> additional burden on solvers (particularly new ones) entering the
>> competition. My personal feeling is that we ought to accept this burden
>> and
>> enable the dual core feature, for the benefit of our applications, and
>> also
>> for the respect of the field: the multicore revolution has been underway
>> for
>> quite some time, and we should officially join it as soon as possible.
>>
>> Please let us know what you think (it is fine to reply to this list, and
>> we
>> can discuss the question here).
>>
>> Aaron
>> on behalf of the SMT-COMP 2010 organizers (Clark Barrett, Morgan Deters,
>> Albert Oliveras, Aaron Stump)
>> _______________________________________________
>> SMT-COMP mailing list
>> SMT-COMP at cs.nyu.edu
>> http://cs.nyu.edu/mailman/listinfo/smt-comp
>>
>>