Thread: [Smtcomp-discussion] FP demo track at SMT-COMP
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
Menu
▾
▴
smtcomp-discussion
|
From: Christoph W. <cw...@mi...> - 2015-06-10 13:08:35
Attachments:
image001.jpg
|
Hi all, So far, none of the submissions to SMT-COMP 2015 have select QF_FP or QF_BVFP as categories they would like to take part in: http://smtcomp.sourceforge.net/2015/participants.shtml We would like to run the floating-point demo track alongside the other competition track, i.e., starting June 14. So, if you would like to participate, please let us know as soon as possible. As Tjark said, if we don't hear from you, your solver(s) will not take part. If you want to take a look at the latest benchmarks before committing to it, they are available on starexec in root/SMT/SMT-LIB benchmarks/2015-06-01/non-incremental/QF_FP and .../QF_BVFP. Thanks, Christoph Tjark Weber tjark.weber at it.uu.se <mailto:smt-comp%40cs.nyu.edu?Subject=Re%3A%20%5BSMT-COMP%5D%20Floating-Point%20Divisions&In-Reply-To=%3C1433712417.3478.33.camel%40it.uu.se%3E> Sun Jun 7 17:26:57 EDT 2015 * Previous message: [SMT-COMP] SMT-COMP 2015: Benchmarks and Tools Available <http://cs.nyu.edu/pipermail/smt-comp/2015/000327.html> * Next message: [SMT-COMP] SMT-COMP 2015: exit Command Optional <http://cs.nyu.edu/pipermail/smt-comp/2015/000329.html> * Messages sorted by: [ date ]<http://cs.nyu.edu/pipermail/smt-comp/2015/date.html#328> [ thread ]<http://cs.nyu.edu/pipermail/smt-comp/2015/thread.html#328> [ subject ]<http://cs.nyu.edu/pipermail/smt-comp/2015/subject.html#328> [ author ]<http://cs.nyu.edu/pipermail/smt-comp/2015/author.html#328> ________________________________ Dear SMT-COMP participants, The recent 2015-06-01 release of SMT-LIB features floating-point benchmarks in two new logics, QF_BVFP and QF_FP. Accordingly, SMT-COMP 2015 will have two experimental floating-point divisions. Please let us know before the final solver deadline on June 14 if you wish to enter your solver(s) into one or both of QF_BVFP and QF_FP. We will not enter your solver(s) into these divisions unless we hear from you, even if you previously entered your solver into "all divisions." Best, Tjark Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter<http://research.microsoft.com/people/cwinter> [MSFT_logo_Gray DE sized SIG1.png] Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB |
|
From: Alberto G. <gr...@fb...> - 2015-06-10 13:24:20
|
Hi, > Hi all, > > So far, none of the submissions to SMT-COMP 2015 have select QF_FP or > QF_BVFP as categories they would like to take part in: > > http://smtcomp.sourceforge.net/2015/participants.shtml > > We would like to run the floating-point demo track alongside the other > competition track, i.e., starting June 14. So, if you would like to > participate, please let us know as soon as possible. As Tjark said, if > we don’t hear from you, your solver(s) will not take part. > > If you want to take a look at the latest benchmarks before committing to > it, they are available on starexec in root/SMT/SMT-LIB > benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP. I was planning to submit. As I told Tjark, I did not understand that the general SMTCOMP deadline was meant also for the FP demo tracks. If I'm still on time, I'll try to submit mathsat by june 14. Alberto |
|
From: Alberto G. <gr...@fb...> - 2015-06-10 15:27:01
|
Hello all, >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or >> QF_BVFP as categories they would like to take part in: >> >> http://smtcomp.sourceforge.net/2015/participants.shtml >> >> We would like to run the floating-point demo track alongside the other >> competition track, i.e., starting June 14. So, if you would like to >> participate, please let us know as soon as possible. As Tjark said, if >> we don’t hear from you, your solver(s) will not take part. >> >> If you want to take a look at the latest benchmarks before committing to >> it, they are available on starexec in root/SMT/SMT-LIB >> benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP. > > I was planning to submit. As I told Tjark, I did not understand that the > general SMTCOMP deadline was meant also for the FP demo tracks. If I'm > still on time, I'll try to submit mathsat by june 14. I have a follow-up question about this. If I understand correctly, fp.min and fp.max are underspecified in the current standard, in the case the inputs are +0 and -0. The reference paper [BTRW15] argues that this is necessary to be fully compliant with IEEE. To me, this seems like an unnecessary complication (for the same reason, I think bit-vector division by 0 should be specified). Regardless of this, however, I found at least one benchmark that seems to be misclassified (there might be more): wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2 Is it too late to ask for a change in the FP standard? Fixing one return value for e.g. (fp.min -0 +0) would make life simpler without losing much IMHO, given that the underspecified semantics can still be encoded if someone really wants that. What do people think? Alberto [BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. |
|
From: Christoph W. <cw...@mi...> - 2015-06-10 15:39:07
|
Regarding fp.min/fp,max in the benchmarks and what's implemented in Z3, please see also this discussion: https://github.com/Z3Prover/z3/issues/68 I agree that we have to fix those to some value, or maybe the second argument. Users can always wrap them in ITEs that select whatever they want for those cases (and internally most of us would do the same kind of wrapping inside our solvers anyways). For the demo track, I think it would be fair to simply exclude that benchmark, so we don't have to find a community consensus right away. Cheers, Christoph Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB -----Original Message----- From: Alberto Griggio [mailto:gr...@fb...] Sent: 10 June 2015 16:27 To: Christoph Wintersteiger; smt...@li...; smt-lib (sm...@cs...) Cc: Martin Brain; Schanda Florian; Florian Lapschies; Pas...@in...; Philipp Ruemmer (phi...@it...); wa...@cc... Subject: Re: FP demo track at SMT-COMP Hello all, >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or >> QF_BVFP as categories they would like to take part in: >> >> http://smtcomp.sourceforge.net/2015/participants.shtml >> >> We would like to run the floating-point demo track alongside the >> other competition track, i.e., starting June 14. So, if you would >> like to participate, please let us know as soon as possible. As Tjark >> said, if we don't hear from you, your solver(s) will not take part. >> >> If you want to take a look at the latest benchmarks before committing >> to it, they are available on starexec in root/SMT/SMT-LIB >> benchmarks/2015-06-01/non-incremental/QF_FP and .../QF_BVFP. > > I was planning to submit. As I told Tjark, I did not understand that > the general SMTCOMP deadline was meant also for the FP demo tracks. If > I'm still on time, I'll try to submit mathsat by june 14. I have a follow-up question about this. If I understand correctly, fp.min and fp.max are underspecified in the current standard, in the case the inputs are +0 and -0. The reference paper [BTRW15] argues that this is necessary to be fully compliant with IEEE. To me, this seems like an unnecessary complication (for the same reason, I think bit-vector division by 0 should be specified). Regardless of this, however, I found at least one benchmark that seems to be misclassified (there might be more): wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2 Is it too late to ask for a change in the FP standard? Fixing one return value for e.g. (fp.min -0 +0) would make life simpler without losing much IMHO, given that the underspecified semantics can still be encoded if someone really wants that. What do people think? Alberto [BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. |
|
From: Martin B. <mar...@cs...> - 2015-06-10 17:19:44
|
On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > Hello all, > > >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or > >> QF_BVFP as categories they would like to take part in: > >> > >> http://smtcomp.sourceforge.net/2015/participants.shtml > >> > >> We would like to run the floating-point demo track alongside the other > >> competition track, i.e., starting June 14. So, if you would like to > >> participate, please let us know as soon as possible. As Tjark said, if > >> we don’t hear from you, your solver(s) will not take part. > >> > >> If you want to take a look at the latest benchmarks before committing to > >> it, they are available on starexec in root/SMT/SMT-LIB > >> benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP. > > > > I was planning to submit. As I told Tjark, I did not understand that the > > general SMTCOMP deadline was meant also for the FP demo tracks. If I'm > > still on time, I'll try to submit mathsat by june 14. > > I have a follow-up question about this. If I understand correctly, > fp.min and fp.max are underspecified in the current standard, in the > case the inputs are +0 and -0. Yes. This is only the cases min(+0,-0) and min(-0,+0) (and the corresponding max cases). > The reference paper [BTRW15] argues that > this is necessary to be fully compliant with IEEE. The specific clause is: <quote> minNum(x, y) is the canonicalized number x if x < y, y if y < x, the canonicalized number if one operand is a number and the other a quiet NaN. Otherwise it is either x or y, canonicalized (this means results might differ among implementations). </quote> Canonicalisation only applies in the case of decimal floating-point which SMT-LIB doesn't (currently) support. My understanding of this is that max and min were not included in the 1985 version of IEEE-754 and that different implementators made different assumptions about what they should do. IIRC the x87 and SSE units on Intel chips have different behaviour, likewise: !(x < y) ? x : y; !(x > y) ? y : x; have different behaviour around +0/-0. > To me, this seems > like an unnecessary complication (for the same reason, I think > bit-vector division by 0 should be specified). Regardless of this, > however, I found at least one benchmark that seems to be misclassified > (there might be more): > > wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2 > > Is it too late to ask for a change in the FP standard? Fixing one return > value for e.g. (fp.min -0 +0) would make life simpler without losing > much IMHO, given that the underspecified semantics can still be encoded > if someone really wants that. What do people think? I, personally, think that we should keep the underspecified semantics as something similar will be needed for converting from float to signed and unsigned integers so it's not as if changing max/min will remove the need to support these. Benchmarks that use this aspect ... should probably be treated like bit-vector divide by 0. Cheers, - Martin |
|
From: Tjark W. <tja...@it...> - 2015-06-10 19:09:41
|
On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > Is it too late to ask for a change in the FP standard? Fixing one return > value for e.g. (fp.min -0 +0) would make life simpler without losing > much IMHO, given that the underspecified semantics can still be encoded > if someone really wants that. What do people think? Fixing one return value while existing IEEE-compliant implementations return different values would be actively harmful in my opinion. It is foreseeable then that users will use fp.min to model IEEE min, that some (if not most) will be unaware of the subtle semantic difference, and that they will ultimately believe they've verified their code when it may well break on some architectures. For the competition, I think the best solution by far is to remove affected benchmarks this year. Are there any other floating-point operators with underspecified semantics that should be removed as well? Best, Tjark |
|
From: Schanda F. <flo...@al...> - 2015-06-11 07:48:42
|
> On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > > Is it too late to ask for a change in the FP standard? Fixing one > return > > value for e.g. (fp.min -0 +0) would make life simpler without losing > > much IMHO, given that the underspecified semantics can still be > encoded > > if someone really wants that. What do people think? > > Fixing one return value while existing IEEE-compliant implementations > return different values would be actively harmful in my opinion. Yes, to add my "industry" voice to this, please keep it as is, that is unspecified. ;) This leaves it up to the tool vendor to specify it, if they happen to know. For example - if I remember right the intel manuals also do not specify what the hardware does. Although, if I remember right, it seems to behave consistently in that it always returns the second (or first?) argument. But fp.min returning -0 and fp.max returning +0 seems an equally likely implementation choice. In fact, I will add some benchmarks to my own testsuite to make sure this behaviour exists. It might all sound a bit silly, but it would be easy enough to construct a program that exploits this behaviour (convert floats to array of bytes) and we would get unsound proofs because of it! Florian |
|
From: Martin B. <mar...@cs...> - 2015-06-11 07:34:19
|
On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > > Is it too late to ask for a change in the FP standard? Fixing one return > > value for e.g. (fp.min -0 +0) would make life simpler without losing > > much IMHO, given that the underspecified semantics can still be encoded > > if someone really wants that. What do people think? > > Fixing one return value while existing IEEE-compliant implementations > return different values would be actively harmful in my opinion. It is > foreseeable then that users will use fp.min to model IEEE min, that > some (if not most) will be unaware of the subtle semantic difference, > and that they will ultimately believe they've verified their code when > it may well break on some architectures. I agree with you but note that there is a counter-argument that in the situation you give, the current semantics will give spurious counter-examples that cannot be executed on the target platform. I guess it is personal taste depending on whether you feel it is better to under or over approximate the behaviour of the system. My reasoning was that all IEEE-754 compliant systems should be model of the theory. > For the competition, I think the best solution by far is to remove > affected benchmarks this year. Are there any other floating-point > operators with underspecified semantics that should be removed as well? (_ fp.to_ubv m), (_ fp.to_sbv m) and fp.to_real are all underspecified for the 'special values' such as +/-Inf and NaN. The first two are also underspecified for all values outside of the current range because, again, there are significant differences in hardware. Cheers, - Martin |
|
From: Tjark W. <tja...@it...> - 2015-06-11 08:15:28
|
On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote: > On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > > Fixing one return value while existing IEEE-compliant implementations > > return different values would be actively harmful in my opinion. It is > > foreseeable then that users will use fp.min to model IEEE min, that > > some (if not most) will be unaware of the subtle semantic difference, > > and that they will ultimately believe they've verified their code when > > it may well break on some architectures. > > I agree with you but note that there is a counter-argument that in the > situation you give, the current semantics will give spurious > counter-examples that cannot be executed on the target platform. I > guess it is personal taste depending on whether you feel it is better to > under or over approximate the behaviour of the system. My reasoning was > that all IEEE-754 compliant systems should be model of the theory. You are right. Do I prefer spurious counter-examples (which users will then look into, and which they can easily rule out with additional assumptions if they want to verify their code against a specific IEEE implementation) over unsound proofs (which users won't notice as unsound until their programs break in production)? Absolutely. Best, Tjark |
|
From: Christoph W. <cw...@mi...> - 2015-06-11 12:31:56
|
There's about an equal number of arguments for both sides in this discussion. My suggestion is to implement whichever is easiest to implement in your solver. We can then add a mandatory command line parameter. If that parameter is not set to any value, we will issue a warning about which semantics are being used and that the user has to set the option even if the default is the right choice. This way, we force the user to explicitly choose the semantics they want (and obviously if they don’t chose anything, they don't care), and we can throw an error if they chose an unsupported option. Cheers, Christoph Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB -----Original Message----- From: Tjark Weber [mailto:tja...@it...] Sent: 11 June 2015 09:15 To: Martin Brain Cc: Alberto Griggio; smt...@li...; smt-lib (sm...@cs...); Christoph Wintersteiger; Florian Lapschies; wa...@cc...; Pas...@in...; Schanda Florian; Philipp Ruemmer (phi...@it...) Subject: Re: [Smtcomp-discussion] FP demo track at SMT-COMP On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote: > On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > > Fixing one return value while existing IEEE-compliant > > implementations return different values would be actively harmful in > > my opinion. It is foreseeable then that users will use fp.min to > > model IEEE min, that some (if not most) will be unaware of the > > subtle semantic difference, and that they will ultimately believe > > they've verified their code when it may well break on some architectures. > > I agree with you but note that there is a counter-argument that in the > situation you give, the current semantics will give spurious > counter-examples that cannot be executed on the target platform. I > guess it is personal taste depending on whether you feel it is better > to under or over approximate the behaviour of the system. My > reasoning was that all IEEE-754 compliant systems should be model of the theory. You are right. Do I prefer spurious counter-examples (which users will then look into, and which they can easily rule out with additional assumptions if they want to verify their code against a specific IEEE implementation) over unsound proofs (which users won't notice as unsound until their programs break in production)? Absolutely. Best, Tjark |
Thanks for helping keep SourceForge clean.
X