[Caml-list] equivalent checking of ocaml program?

[Caml-list] equivalent checking of ocaml program?

[沈胜宇]

[-- Attachment #1: Type: text/plain, Size: 203 bytes --]

Dear all:


I am working hard to optimize my ocaml program, but I am not sure whether the significantly modified version is equal to the old version.


So is there any research work on this topic?


Shen

[-- Attachment #2: Type: text/html, Size: 272 bytes --]

Re: [Caml-list] equivalent checking of ocaml program?

[David Allsopp]

> On 29 Sep 2013, at 13:07, "沈胜宇" <syshen@nudt.edu.cn> wrote:
> 
> Dear all:
> 
> I am working hard to optimize my ocaml program, but I am not sure whether the significantly modified version is equal to the old version.

By equal, you mean equivalent?

> So is there any research work on this topic?

There was in the 1920s and 1930s by a few chaps called Turing, Church and Gödel :)

Have a search for the halting problem (or the Entscheidungsproblem, for its motivation)


David

> 
> Shen

Re: [Caml-list] equivalent checking of ocaml program?

[mukesh tiwari]

[-- Attachment #1: Type: text/plain, Size: 815 bytes --]

Hi Syshen,
I am not sure if it's answer to your question but the problem is
undecidable although you can use SMT solver to verify both of your program.
I don't have idea using SMT solver in OCaml ( right now I am learning it )
but I used it Haskell[1]. You can ask SMT solver to find a counter case for
which your both programs are not producing the same output. If it gives you
the such case then certainly your both code is not same.


-Mukesh Tiwari
[1] http://hackage.haskell.org/package/sbv-2.10


On Sun, Sep 29, 2013 at 4:29 PM, 沈胜宇 <syshen@nudt.edu.cn> wrote:

> Dear all:
>
> I am working hard to optimize my ocaml program, but I am not sure whether
> the significantly modified version is equal to the old version.
>
> So is there any research work on this topic?
>
> Shen
>

[-- Attachment #2: Type: text/html, Size: 1259 bytes --]

Re: [Caml-list] equivalent checking of ocaml program?

[Robert Jakob]

Well, the typical approach is to write a test suite before refactoring
and ensure that the test suite runs without errors before and after the
refactoring.

To be sure that the program really behaves like before, you need to
have a good (whatever this means) test suite.

And as others have mentioned, due to the Halting problem this can only
be an approximation in general.

r.

On Sun, 29 Sep 2013 18:59:11 +0800 (GMT+08:00)
沈胜宇 <syshen@nudt.edu.cn> wrote:

> Dear all:
> 
> 
> I am working hard to optimize my ocaml program, but I am not sure
> whether the significantly modified version is equal to the old
> version.
> 
> 
> So is there any research work on this topic?
> 
> 
> Shen
> 

Re: [Caml-list] equivalent checking of ocaml program?

[Florent Monnier]

2013/09/29, Robert Jakob wrote:
> Well, the typical approach is to write a test suite before refactoring
> and ensure that the test suite runs without errors before and after the
> refactoring.
>
> To be sure that the program really behaves like before, you need to
> have a good (whatever this means) test suite.

It may also be recommanded to keep the simple code next to the optimised one.
It can be useful for many reasons. For example for the tests (compare
them), you can also use it as a failsafe alternative if the optimised
version fails. For the people who will try to read and understand your
code in the future (one of them might be you).

-- 
bp.

Re: [Caml-list] equivalent checking of ocaml program?

[沈胜宇]

I dont think approach based on testing is a good solution, although I have used it for a long time.
This appraoch miss many conner case, which leads to error long after modification and cost lots of time in debugging.

For the halting problem, I also dont think it can prevent us from solving equivalent problem. Some undecidable problem, such as termination checking, have been studied by bryon cook for a long time, and it can check termination successfully for many programs. of course, it is not complete, but most program written manually have some fixed pattern, not totally random.

for checking equivalent of ocaml program, most of my modification to my program also have some fixed pattern, for example, using hash table indexing to replace list searching. I think smt can solve it easily. May be I need to solve it by my self?

Shen


> -----原始邮件-----
> 发件人: "Florent Monnier" <monnier.florent@gmail.com>
> 发送时间: 2013-09-30 00:19:29 (星期一)
> 收件人: "沈胜宇" <syshen@nudt.edu.cn>
> 抄送: caml-list@inria.fr
> 主题: Re: [Caml-list] equivalent checking of ocaml program?
> 
> 2013/09/29, Robert Jakob wrote:
> > Well, the typical approach is to write a test suite before refactoring
> > and ensure that the test suite runs without errors before and after the
> > refactoring.
> >
> > To be sure that the program really behaves like before, you need to
> > have a good (whatever this means) test suite.
> 
> It may also be recommanded to keep the simple code next to the optimised one.
> It can be useful for many reasons. For example for the tests (compare
> them), you can also use it as a failsafe alternative if the optimised
> version fails. For the people who will try to read and understand your
> code in the future (one of them might be you).
> 
> -- 
> bp.

Re: [Caml-list] equivalent checking of ocaml program?

[Goswin von Brederlow]

On Mon, Sep 30, 2013 at 08:26:46AM +0800, ?????? wrote:
> I dont think approach based on testing is a good solution, although I have used it for a long time.
> This appraoch miss many conner case, which leads to error long after modification and cost lots of time in debugging.

Then your test suite was bad. You need enough tests to cover every
code path in your code and then some. Obviously in any complex code
you will forget / miss some. But over time your tests will improve too.

> For the halting problem, I also dont think it can prevent us from solving equivalent problem. Some undecidable problem, such as termination checking, have been studied by bryon cook for a long time, and it can check termination successfully for many programs. of course, it is not complete, but most program written manually have some fixed pattern, not totally random.
> 
> for checking equivalent of ocaml program, most of my modification to my program also have some fixed pattern, for example, using hash table indexing to replace list searching. I think smt can solve it easily. May be I need to solve it by my self?
> 
> Shen
> 
> 
> > -----????????-----
> > ??????: "Florent Monnier" <monnier.florent@gmail.com>
> > ????????: 2013-09-30 00:19:29 (??????)
> > ??????: "??????" <syshen@nudt.edu.cn>
> > ????: caml-list@inria.fr
> > ????: Re: [Caml-list] equivalent checking of ocaml program?
> > 
> > 2013/09/29, Robert Jakob wrote:
> > > Well, the typical approach is to write a test suite before refactoring
> > > and ensure that the test suite runs without errors before and after the
> > > refactoring.
> > >
> > > To be sure that the program really behaves like before, you need to
> > > have a good (whatever this means) test suite.
> > 
> > It may also be recommanded to keep the simple code next to the optimised one.
> > It can be useful for many reasons. For example for the tests (compare
> > them), you can also use it as a failsafe alternative if the optimised
> > version fails. For the people who will try to read and understand your
> > code in the future (one of them might be you).

I sometimes write a wrapper module around the code that runs both the
old and new code and compares the result. Only when both return the
same the value is returned. Run that with a large enough test suite or
simply use it for a while and you get good test coverage without
having to define input and output values.

MfG
	Goswin

Re: [Caml-list] equivalent checking of ocaml program?

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 4847 bytes --]

This thread may be a good opportunity to advertize for some work on static
program verification that has been applied to OCaml (sadly, it is actually
quite rare to see program verification efforts for functional programming
languages, in large part because funding bodies and reviewers appreciate
applications to mainstream language with larger codebases). I am aware of
the following, feel free to add more suggestions:
- MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/
  Based on foundational work on model-checking of higher-order programs by
Ong, Kobayashi and others (see the citations of the papers on the webpage),
MoCHi can work with a subset of OCaml. It is not ready to handle real-world
programs, both in term of verification time and the ocaml feature it
understands, but going in the right direction -- and the underlying tools
are rapidly improving, see e.g. the recent work on C-SHORe
- Hybrid Contract Checking for OCaml, by Dana Xu
http://gallium.inria.fr/~naxu/research/hcc.html
  (I previosuly mentioned on this list the available prototype that extends
OCaml with dynamic contract checking)

Another brand of work making good progress is the "Liquid Types" project in
San Diego ( http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ ),
which are working on applications to Haskell.

Note that those tools are generally aimed at checking that programs respect
some safety condition (eg. "does not end in an assertion failure"), not
general specifications or general equivalence checking. You may consider
encoding general equivalence checking in these term (traverse the input
space and assert that the output of both functions are equivalent), but I
don't know if the tools can handle the encoding efficiently. If you want
full functional correctness for higher-order programs, rather than
automated safety checkers, I would probably rather look at proof-assistant
frameworks (eg. Ynot http://ynot.cs.harvard.edu/ or CFML
http://www.chargueraud.org/softs/cfml/ ).



On Mon, Sep 30, 2013 at 4:53 PM, Goswin von Brederlow <goswin-v-b@web.de>wrote:

> On Mon, Sep 30, 2013 at 08:26:46AM +0800, ?????? wrote:
> > I dont think approach based on testing is a good solution, although I
> have used it for a long time.
> > This appraoch miss many conner case, which leads to error long after
> modification and cost lots of time in debugging.
>
> Then your test suite was bad. You need enough tests to cover every
> code path in your code and then some. Obviously in any complex code
> you will forget / miss some. But over time your tests will improve too.
>
> > For the halting problem, I also dont think it can prevent us from
> solving equivalent problem. Some undecidable problem, such as termination
> checking, have been studied by bryon cook for a long time, and it can check
> termination successfully for many programs. of course, it is not complete,
> but most program written manually have some fixed pattern, not totally
> random.
> >
> > for checking equivalent of ocaml program, most of my modification to my
> program also have some fixed pattern, for example, using hash table
> indexing to replace list searching. I think smt can solve it easily. May be
> I need to solve it by my self?
> >
> > Shen
> >
> >
> > > -----????????-----
> > > ??????: "Florent Monnier" <monnier.florent@gmail.com>
> > > ????????: 2013-09-30 00:19:29 (??????)
> > > ??????: "??????" <syshen@nudt.edu.cn>
> > > ????: caml-list@inria.fr
> > > ????: Re: [Caml-list] equivalent checking of ocaml program?
> > >
> > > 2013/09/29, Robert Jakob wrote:
> > > > Well, the typical approach is to write a test suite before
> refactoring
> > > > and ensure that the test suite runs without errors before and after
> the
> > > > refactoring.
> > > >
> > > > To be sure that the program really behaves like before, you need to
> > > > have a good (whatever this means) test suite.
> > >
> > > It may also be recommanded to keep the simple code next to the
> optimised one.
> > > It can be useful for many reasons. For example for the tests (compare
> > > them), you can also use it as a failsafe alternative if the optimised
> > > version fails. For the people who will try to read and understand your
> > > code in the future (one of them might be you).
>
> I sometimes write a wrapper module around the code that runs both the
> old and new code and compares the result. Only when both return the
> same the value is returned. Run that with a large enough test suite or
> simply use it for a while and you get good test coverage without
> having to define input and output values.
>
> MfG
>         Goswin
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 6514 bytes --]

Re: [Caml-list] equivalent checking of ocaml program?

[Robert Jakob]

On Mon, 30 Sep 2013 17:49:11 +0200
Gabriel Scherer <gabriel.scherer@gmail.com> wrote:

> This thread may be a good opportunity to advertize for some work on
> static program verification that has been applied to OCaml (sadly, it
> is actually quite rare to see program verification efforts for
> functional programming languages, in large part because funding
> bodies and reviewers appreciate applications to mainstream language
> with larger codebases). I am aware of the following, feel free to add
> more suggestions:
> - MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/
>   Based on foundational work on model-checking of higher-order
> programs by Ong, Kobayashi and others (see the citations of the
> papers on the webpage), MoCHi can work with a subset of OCaml. It is
> not ready to handle real-world programs, both in term of verification
> time and the ocaml feature it understands, but going in the right
> direction -- and the underlying tools are rapidly improving, see e.g.
> the recent work on C-SHORe
The approaches by Ong, Kobayashi, Broadbent et al. work on higher-order
recursion schemes (HORS) to represent output/states of functional
programs. Yet, it is not known if the equivalence of two HORS is
decidable. So this might be applicable to deciding the equivalency of
ocaml programs (wrt. outputs/state), but it is not clear.

r.

Re: [Caml-list] equivalent checking of ocaml program?

[Gabriel Scherer]

Shortly after writing my email, I found out that Ong had co-written a
recent article (CAV'12) on using those techniques precisely for
equivalence checking:

  Hector: An Equivalence Checker for a Higher-Order Fragment of ML
  David Hopkins' Andrzej S. Murawski and C.-H Luke Ong
  2012
  http://www.cs.ox.ac.uk/files/4786/cav12.pdf

They restrict themselves to a order-bounded fragment of higher-order
function types (and only allow ground reference types) suggested by
game-semantics considerations, on which equivalence checking is
decidable, and leave extensions to more complex settings where
equivalence becomes indecidable to future work.
You probably know more about this than I do (this is not my field at
all), but my understanding is that whether the problems are decidable
or not is not an actual concern with model checking, as even in
decidable cases the tools most often run out of time; actual
feasability on concrete examples seems the most useful way to evaluate
those, so I don't think going to undecidable fragments would be a
problem in principle. Of course, the more complex the fragment, the
more expansive the computations.

On Tue, Oct 8, 2013 at 3:27 PM, Robert Jakob <rj@robertjakob.de> wrote:
> On Mon, 30 Sep 2013 17:49:11 +0200
> Gabriel Scherer <gabriel.scherer@gmail.com> wrote:
>
>> This thread may be a good opportunity to advertize for some work on
>> static program verification that has been applied to OCaml (sadly, it
>> is actually quite rare to see program verification efforts for
>> functional programming languages, in large part because funding
>> bodies and reviewers appreciate applications to mainstream language
>> with larger codebases). I am aware of the following, feel free to add
>> more suggestions:
>> - MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/
>>   Based on foundational work on model-checking of higher-order
>> programs by Ong, Kobayashi and others (see the citations of the
>> papers on the webpage), MoCHi can work with a subset of OCaml. It is
>> not ready to handle real-world programs, both in term of verification
>> time and the ocaml feature it understands, but going in the right
>> direction -- and the underlying tools are rapidly improving, see e.g.
>> the recent work on C-SHORe
> The approaches by Ong, Kobayashi, Broadbent et al. work on higher-order
> recursion schemes (HORS) to represent output/states of functional
> programs. Yet, it is not known if the equivalence of two HORS is
> decidable. So this might be applicable to deciding the equivalency of
> ocaml programs (wrt. outputs/state), but it is not clear.
>
> r.
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs