(4 intermediate revisions by 3 users not shown) | |||
Line 1: | Line 1: | ||
[[Category:Developer Manual]] | [[Category:Developer Manual]] | ||
__NOTOC__ | __NOTOC__ | ||
In this chapter we try to answer the question: why did we use Prolog to develop the core of ProB, and in particular why do we use the commercial [ | In this chapter we try to answer the question: why did we use Prolog to develop the core of ProB, and in particular why do we use the commercial [https://sicstus.sics.se/ SICStus Prolog] rather than an open-source alternative. | ||
The short answer is that Prolog allows us to flexibly implement various specification formalisms as well as the analysis and verification tools that go along with it. At the same time, Prolog is very fast and SICStus Prolog is one of the fastest and most stable Prolog systems | The short answer is that Prolog allows us to flexibly implement various specification formalisms as well as the analysis and verification tools that go along with it. At the same time, Prolog is very fast and SICStus Prolog is one of the fastest and most stable Prolog systems, allows access to more than | ||
256 MB of heap even on 32 bit systems (important for model checking), | 256 MB of heap even on 32 bit systems (important for model checking), | ||
and is easy to interate with other programming languages | and is easy to interate with other programming languages | ||
Line 9: | Line 9: | ||
== Why Prolog == | == Why Prolog == | ||
* Prolog is a convenient language to express the semantics of other languages | * Prolog is a convenient language in which to express the semantics of other languages. | ||
:In particular, high-level languages with non-determinism can be expressed with an ease that is hard to match by other languages. For example, the ProB source code to encode the semantics of the internal choice (encoded internally as '|') from CSP is basically as follows: | :In particular, high-level languages with non-determinism can be expressed with an ease that is hard to match by other languages. For example, the ProB source code to encode the semantics of the internal choice (encoded internally as '|') from CSP is basically as follows: | ||
cspm_trans('|'(X,_Y),tau,X). | cspm_trans('|'(X,_Y),tau,X). | ||
Line 20: | Line 20: | ||
:- block less_than_equal(-,?), less_than_equal(?,-). | :- block less_than_equal(-,?), less_than_equal(?,-). | ||
less_than_equal(X,Y) :- X=<Y. | less_than_equal(X,Y) :- X=<Y. | ||
:A nice aspect is that the block declarations do *not* influence the declarative semantics of a Prolog program | :A nice aspect is that the block declarations do *not* influence the declarative semantics of a Prolog program because of the theorem which states that the declarative semantics of logic programs is independent of the selection rule. | ||
I believe this to be one of the "killer" | I believe this to be one of the "killer" features of modern Prolog systems. | ||
We heavily use this in the ProB kernel to delay enumeration of values | We heavily use this in the ProB kernel to delay enumeration of values | ||
and to implement our own constraint solver over sets and relations. | and to implement our own constraint solver over sets and relations. | ||
Line 29: | Line 29: | ||
* Prolog is fast. | * Prolog is fast. | ||
:This may be surprising to some | :This may be surprising to some as Prolog sometimes has a reputation of being slow. On the laptop used for the experiments below, SICStus Prolog can perfrom 33 Million logical inferences per second (on my very latest laptop in can actually perform 75 Million logical inferences per second in 64-bit mode). As you see below, it can sometimes be faster than Java. Modern Prolog systems are well tuned and developed, and will outperform your own logical inference or unification mechanism by a considerable margin (I observed a factor of 10,000 between SICStus Prolog and the C implementation of a custom rule engine in a commercial product). | ||
In summary, Prolog gives us both a flexible way to encode both the operational | In summary, Prolog gives us both a flexible way to encode both the operational | ||
Line 42: | Line 42: | ||
libraries is not ideal (the ISO standard does not cover the module system | libraries is not ideal (the ISO standard does not cover the module system | ||
for one). There is no standard static type checking tool. | for one). There is no standard static type checking tool. | ||
* Prolog is concise | |||
See my [[Prolog vs Java Comparison]] on some sample code from ProB2-UI | |||
== Why SICStus Prolog == | == Why SICStus Prolog == | ||
Line 93: | Line 96: | ||
* - commercial | * - commercial | ||
B Prolog | B Prolog | ||
* - no Bigints | * - no Bigints prior to version 7.6, but now available | ||
* + constraint-based graphics library | * + constraint-based graphics library | ||
* - commercial (but free academic license) | * - commercial (but free academic license) | ||
* + has action-rule mechanism (which apparently is a co-routining mechanism; I have not yet been able to experiment with it) | |||
Other Prologs | Other Prologs with which I have not directly experimented are: Visual Prolog and IF Prolog. | ||
It seems that maybe Yap and SWI are merging efforts. It would be nice to have a Prolog system with the features of SWI and the speed of YAP. This would be a serious (free) alternative to SICStus Prolog. | It seems that maybe Yap and SWI are merging efforts. It would be nice to have a Prolog system with the features of SWI and the speed of YAP. This would be a serious (free) alternative to SICStus Prolog. | ||
Line 104: | Line 108: | ||
== A small benchmark == | == A small benchmark == | ||
Below I have conducted a small experiment | Below I have conducted a small experiment to gauge the performance | ||
of various Prolog systems. I do not claim that this example | of various Prolog systems. I do not claim that this example | ||
is representative; it tests only a few aspects of performance | is representative; it tests only a few aspects of performance | ||
Line 110: | Line 114: | ||
a more extensive evaluation at the moment. | a more extensive evaluation at the moment. | ||
The benchmark is the Fibonacci function | The benchmark is the Fibonacci function written in the naive | ||
recursive way so as to quickly obtain a large number of recursive | recursive way so as to quickly obtain a large number of recursive | ||
calls. The advantage is that the code can be easily transcribed | calls. The advantage is that the code can be easily transcribed | ||
into other programming languages. Below, I give you also a | into other programming languages. Below, I give you also a | ||
Python, Haskell and a Java version using BigInts. | Python, a Haskell, and a Java version using BigInts. | ||
The benchmarks were run on a MacBook Pro Core2 Duo with 2.33 GHz. | The benchmarks were run on a MacBook Pro Core2 Duo with 2.33 GHz. | ||
BinProlog does not have a demo licence for Mac; hence I had to run | BinProlog does not have a demo licence for Mac; hence I had to run | ||
the Windows version in Parallels. LPA Prolog only runs on Windows; so | the Windows version in Parallels. LPA Prolog only runs on Windows; so | ||
it was also run using Parallels. | it was also run using Parallels. | ||
Note | Note: the purpose of the benchmark was to measure the performance | ||
of recursion. As such, I was trying to use the same | of recursion. As such, I was trying to use the same types of data on all | ||
platforms (BigInts). | platforms (BigInts). | ||
Also | Also note that this is actually not a typical Prolog "application" as no | ||
use is made of unification or non-determinism. But it is a good application | use is made of unification or non-determinism. But it is a good application | ||
for a functional programming language such as Haskell | for a functional programming language such as Haskell since Fibonacci is | ||
a pure function without side-effects. | a pure function without side-effects. | ||
Also, I do not claim that the benchmark shows that Prolog is faster than Java in general. | Also, I do not claim that the benchmark shows that Prolog is faster than Java in general. | ||
My only claim is that | My only claim is that if an application is well suited to Prolog, its | ||
performance can be surprisingly good. I also have the feeling that | performance can be surprisingly good. I also have the feeling that | ||
Haskell has made great strides in performance recently, and that | Haskell has made great strides in performance recently, and that | ||
Line 223: | Line 227: | ||
time sicstus --goal "halt." | time sicstus --goal "halt." | ||
For SWI Prolog 5.6.64 we get 0.015 s real time (0.008 s user time): | For SWI Prolog 5.6.64, we get 0.015 s real time (0.008 s user time): | ||
time swipl -g "halt." | time swipl -g "halt." | ||
For Ciao Prolog 1.13.0-8334 we get 0.271 s user time for "time ciao" and then typing halt | For Ciao Prolog 1.13.0-8334, we get 0.271 s user time for "time ciao" and then typing halt | ||
(I found no easy way to provide goals on the command-line). | (I found no easy way to provide goals on the command-line). | ||
Line 236: | Line 240: | ||
time sicstus -l halt.pl | time sicstus -l halt.pl | ||
The following takes 0.204 seconds real time the first time | The following takes 0.204 seconds real time the first time and 0.015 seconds real time the second time: | ||
time swipl -c halt.pl | time swipl -c halt.pl | ||
The following takes 0.726 seconds real time | The following takes 0.726 seconds real time and 0.648 seconds user time (after commenting out :- main.), i.e., 25 times slower than SICStus: | ||
time ciao -c halt.pl | time ciao -c halt.pl |
In this chapter we try to answer the question: why did we use Prolog to develop the core of ProB, and in particular why do we use the commercial SICStus Prolog rather than an open-source alternative.
The short answer is that Prolog allows us to flexibly implement various specification formalisms as well as the analysis and verification tools that go along with it. At the same time, Prolog is very fast and SICStus Prolog is one of the fastest and most stable Prolog systems, allows access to more than 256 MB of heap even on 32 bit systems (important for model checking), and is easy to interate with other programming languages (so that the GUI does not have to be developed in Prolog).
cspm_trans('|'(X,_Y),tau,X). cspm_trans('|'(_X,Y),tau,Y).
:- block less_than_equal(-,?), less_than_equal(?,-). less_than_equal(X,Y) :- X=<Y.
I believe this to be one of the "killer" features of modern Prolog systems. We heavily use this in the ProB kernel to delay enumeration of values and to implement our own constraint solver over sets and relations. In my experience, this feature allows one to write much more declarative code than with traditional Prolog systems (an example is the transcription of Roscoe's operational semantics mentioned above), while often obtaining a dramatic increase in performance in generate-and-test scenarios.
In summary, Prolog gives us both a flexible way to encode both the operational semantics of many high-level formalisms (B, Z, CSP, ...) and various flexible tools on top such as animation, type checking, model checking and refinement checking.
All of this comes with a respectable performance, despite the flexibility of the approach.
There are of course still aspects with Prolog that, despite many years of research and development, are not ideal. Standardisation of Prolog and the libraries is not ideal (the ISO standard does not cover the module system for one). There is no standard static type checking tool.
See my Prolog vs Java Comparison on some sample code from ProB2-UI
Below is a short summary of some of the Prolog systems that to my knowledge are still being actively maintained (please email me corrections and additions).
SICStus:
SWI
Ciao
Gnu Prolog
XSB Prolog:
Yap
LPA
BinProlog
B Prolog
Other Prologs with which I have not directly experimented are: Visual Prolog and IF Prolog.
It seems that maybe Yap and SWI are merging efforts. It would be nice to have a Prolog system with the features of SWI and the speed of YAP. This would be a serious (free) alternative to SICStus Prolog.
Below I have conducted a small experiment to gauge the performance of various Prolog systems. I do not claim that this example is representative; it tests only a few aspects of performance (e.g., speed of recursive calls). I don't have the time to do a more extensive evaluation at the moment.
The benchmark is the Fibonacci function written in the naive recursive way so as to quickly obtain a large number of recursive calls. The advantage is that the code can be easily transcribed into other programming languages. Below, I give you also a Python, a Haskell, and a Java version using BigInts. The benchmarks were run on a MacBook Pro Core2 Duo with 2.33 GHz. BinProlog does not have a demo licence for Mac; hence I had to run the Windows version in Parallels. LPA Prolog only runs on Windows; so it was also run using Parallels. Note: the purpose of the benchmark was to measure the performance of recursion. As such, I was trying to use the same types of data on all platforms (BigInts). Also note that this is actually not a typical Prolog "application" as no use is made of unification or non-determinism. But it is a good application for a functional programming language such as Haskell since Fibonacci is a pure function without side-effects.
Also, I do not claim that the benchmark shows that Prolog is faster than Java in general. My only claim is that if an application is well suited to Prolog, its performance can be surprisingly good. I also have the feeling that Haskell has made great strides in performance recently, and that the Prolog community should be on its guard (so as not to be left behind).
System BigInts Fib(30) Fib(35) Java 1.5.0_16 NO (long) 0.020 0.231 GHC 6.10.1 yes 0.082 0.878 Yap 5.1.3 NO 0.193 2.112 SICStus 4.0.4 yes 0.240 2.640 Ciao 1.13.0 yes 0.312 3.461 BinProlog 11.38 NO 0.361 3.725 Java 1.5.0_16 yes 0.445 4.898 XSB 3.1 NO 0.456 5.064 Python 2.5.1 yes 0.760 8.350 Gnu 1.3.1 NO 1.183 13.139 SWI 5.6.52 yes 1.900 20.990 LPA 4.710 yes 1.736 36.250
The same table with only the BigInteger versions is:
System BigInts Fib(30) Fib(35) GHC 6.10.1 yes 0.082 0.878 SICStus 4.0.4 yes 0.240 2.640 Ciao 1.13.0 yes 0.312 3.461 Java 1.5.0_16 yes 0.445 4.898 Python 2.5.1 yes 0.760 8.350 SWI 5.6.52 yes 1.900 20.990 LPA 4.710 yes 1.736 36.250
I have also recently tested B Prolog 7.4. It seems to perform marginally faster than SICStus (3 %), but does not support BigInts. Note, that Gnu is the only system requiring tweaking of parameters:
export TRAILSZ=200000 export GLOBALSZ=1500000
Java with int rather than BigIntegers takes 0.016 s for Fib(30) and 0.163 s for Fib(35). Note that GHC Haskell seems to have received a big performance boost on this particular example (earlier versions of Haskell were on par with SICStus Prolog).
I also wanted to experiment with a Mercury version, but for the moment Mercury does not compile/install on my machine. Marc Fontaine has also written various Haskell versions of Fibonacci
Here are the various versions of Fibonacci:
Prolog Version:
fib(0,1) :- !. fib(1,1) :- !. fib(N,R) :- N1 is N-1, N2 is N1-1, fib(N1,R1), fib(N2,R2), R is R1+R2.
Python Version:
def Fib(x): if x<2: return 1 else: return Fib(x-1)+Fib(x-2)
Java Version with BigInteger:
private static BigInteger ZERO = BigInteger.ZERO; private static BigInteger ONE = BigInteger.ONE; private static BigInteger TWO = new BigInteger("2"); public static BigInteger naiveFib(BigInteger x) { if (x.equals(ZERO) ) return ONE; if (x.equals(ONE) ) return BigInteger.ONE; return naiveFib(x.subtract(ONE)).add(naiveFib(x.subtract(TWO))); }
Haskell Version:
fib :: Integer -> Integer fib n | n == 0 = 1 | n == 1 = 1 | otherwise = fib(n-1) + fib(n-2)
Java Version with long rather than BigIntegers:
public static long fib(long xx) { if (xx<2) return 1; else return fib(xx-1)+fib(xx-2); }
Below we test the startup times of some of the Prolog systems. Unfortunately, not all Prolog systems can easily be started as easily from the command-line as SICStus Prolog (e.g., --goal "GOAL." parameter and -l FILE parameter).
First, the following command takes 0.026 s real time (0.015 s user time) with SICStus Prolog 4.0.5 on the same system as above:
time sicstus --goal "halt."
For SWI Prolog 5.6.64, we get 0.015 s real time (0.008 s user time):
time swipl -g "halt."
For Ciao Prolog 1.13.0-8334, we get 0.271 s user time for "time ciao" and then typing halt (I found no easy way to provide goals on the command-line).
Now, take the file halt.pl with contents:
main :- print(hello),nl,halt. :- main.
The following takes 0.028 seconds real time and 0.015 seconds user time.
time sicstus -l halt.pl
The following takes 0.204 seconds real time the first time and 0.015 seconds real time the second time:
time swipl -c halt.pl
The following takes 0.726 seconds real time and 0.648 seconds user time (after commenting out :- main.), i.e., 25 times slower than SICStus:
time ciao -c halt.pl