Bug 486757 - Review Request: divine-mc - Multi-core model checking system for proving specifications
Summary: Review Request: divine-mc - Multi-core model checking system for proving spec...
Keywords:
Status: CLOSED WONTFIX
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Milos Jakubicek
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2009-02-21 20:36 UTC by David A. Wheeler
Modified: 2011-02-19 10:28 UTC (History)
4 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2011-02-19 10:28:33 UTC
Type: ---
Embargoed:
xjakub: fedora-review?


Attachments (Terms of Use)

Description David A. Wheeler 2009-02-21 20:36:14 UTC
Spec URL: http://www.dwheeler.com/divine-mc.spec
SRPM URL: http://www.dwheeler.com/divine-mc-1.3-1.fc10.src.rpm
Description:
DiVinE Multi-Core (MC) is a parallel shared-memory enumerative model-checking
tool for verification of concurrent systems. The tool can employ the full
power of modern 64-bit multi-core architectures.
It can be used to prove correctness of verification models as
well as to detect early design errors.

Any model-checking tool, such as DiViNe MC, accepts system requirements or
design (called models) and a property (called specification) that the final
system is expected to satisfy. The tool then outputs yes if the given
model satisfies given specifications, and generates a counterexample
otherwise. The counterexample details why the model doesn't satisfy
the specification.

DiViNe MC is based on automata-theoretic approach to
linear temporal logics (LTL) model checking.
The input language allows for specification of processes in terms of
extended finite automata and the verified system is then obtained as
an asynchronous parallel composition of these processes.

In the current DiVinE Multi-Core release, input is provided in DVE format --
an industry-strength specification language, as used in original
DiVinE, with plenty of diverse example models, ranging from simple toys
to complex real-world models. An extensive model database is available
at BEEM database.

Moreover, DiVinE can read models specified in ProMeLa (as used in the SPIN
tool), in addition to its native DVE format. However, the capabilities of
the tool on ProMeLa models is currently limited by inability to produce
counterexamples: you can only obtain a yes/no answer.

Comment 1 David A. Wheeler 2009-02-24 05:21:40 UTC
Sorry, here's an updated spec/SRPM pair:

Spec URL: http://www.dwheeler.com/divine-mc.spec
SRPM URL: http://www.dwheeler.com/divine-mc-1.3-2.fc10.src.rpm

This program doesn't build on ppc64, but the previous specification accidentally omitted the required ExcludeArch.  This revision 2 adds the ExcludeArch (I had trouble accessing Koji earlier, or I would've found this earlier.)

Clean bill of health building on Koji; as noted at:
 http://koji.fedoraproject.org/koji/taskinfo?taskID=1151799
1151799 build (dist-f10, divine-mc-1.3-2.fc10.src.rpm): open (x86-3.fedora.phx.redhat.com) -> closed
  0 free  0 open  4 done  0 failed

rpmlint gives a clean bill of health, too.

Comment 2 Milos Jakubicek 2009-03-02 00:51:39 UTC
Please, first of all, make the package build in current rawhide, the package doesn't build with gcc 4.4 (this has nothing to do with the ppc64 debuginfo failure):

http://koji.fedoraproject.org/koji/taskinfo?taskID=1212023

(hopefully it will be enough to add the necessary headers, if you don't know what to do, just tell me)

I'll then try to narrow the ppc64 debuginfo issue.

Comment 3 David A. Wheeler 2009-03-03 03:13:46 UTC
Thanks.  I've fixed it, including the ppc64 issue.  It now packages for all architectures on both dist-f10 and dist-f11 (using koji build --scratch).

The Rawhide problem was primarily because the new gcc 4.4 is much stricter about C++ headers.  Basically, you HAVE to #include <cstdio> if you use stuff that's defined there (like EOF).  In previous gcc's, many other #includes also quietly brought in these definitions.  gcc's new behavior is correct, but I think we'll see LOTS of C++ patches for this Fedora release (!).  There's also a change in the flex++ API that I had to resolve.  This was unfun to work around, but I think I've got it.  I also added throw() definitions for 2 mallocs as an optimization/cleanup, courtesy of some Ubuntu feedback.

In the process, I think also managed to solve the ppc64 debuginfo problem.  It turns out that if you invoke gcc with "-gstabs+", the debuginfo process will fail.  This happens on x86_64 on rawhide, too.  It's a known Fedora bug:
https://bugzilla.redhat.com/show_bug.cgi?id=453506

Here's the koji scratch build for dist-f11:
 http://koji.fedoraproject.org/koji/taskinfo?taskID=1215612
Koji scratch build for dist-f10:
 http://koji.fedoraproject.org/koji/taskinfo?taskID=1215692

They're rpmlint-clean; I did rpmlint on the .spec, the SRPM, and divine-mc-1.3-3.fc11.x86_64.rpm.

Here's the updated spec and SRPM:
Spec URL: http://www.dwheeler.com/divine-mc.spec
SRPM URL: http://www.dwheeler.com/divine-mc-1.3-3.fc10.src.rpm

Comment 4 Petr Rockai 2009-03-03 09:41:16 UTC
Hi,

I suppose it is generally fine, however please note I don't have a fedora installation handy where I could test the packages. You might also want to consider checking that the outcome of the tests you put in %check is correct (you can use --report and some simple grepping for that).

Actually, DiVinE 2.0 will come with a bunch of unit and functional tests bundled, so running those will be probably preferable. First release on the 2.0 branch is planned in a course of few weeks. However, looking at http://fedoraproject.org/wiki/Releases/11/Schedule I guess we will miss Fedora 11 with that release, so adding a few checks to the spectime in the meantime would be nice. Cf.
https://anna.fi.muni.cz/divine/trac/browser/test/reachability.sh
https://anna.fi.muni.cz/divine/trac/browser/test/owcty.sh

Thanks!

Comment 5 David A. Wheeler 2009-03-04 05:56:56 UTC
I'll be glad to package DiVinE 2.0 when it's out.  My experience is that deadlines often get missed :-).  So, let's package what's available.  If nothing else, packaging the next release is likely to get way easier.

I'll try to improve the automated tests, though, as you suggested.

Comment 6 Milos Jakubicek 2009-03-04 23:50:23 UTC
OK, there are some more outstanding problems:

- patches: Please put the patch3 (gcc4.4) and patch4(flex) also into upstreams bugtracker system and paste the link into spec file. The patches are well commented, however, the comments are usually put directly to the "PatchX:" section in the beginning of the spec file. It would be nice if you follow this habit as described on:
https://fedoraproject.org/wiki/PackagingDrafts/PatchUpstreamStatus

- gcc flags: because you can't use the %configure macro, you have to add 'export CXXFLAGS="%{optflags}" CFLAGS="%{optflags}"' before calling configure to ensure that the flags are propagated. You don't need to call it in "make CXXFLAGS..." then.
Moreover you should remove -fomit-frame-pointer (this is prohibited in Fedora, it makes debugging harder or impossible) and -pipe+ (gcc doesn't seem to know it -- don't know what's the difference to -pipe which is in Fedoras standard gcc flags).

- please remove the "true --libdir=%{_libdir}", this is not a rpmlint bug, rpmlint is not intended to have always right: it just prints a warning then, which is completely ok as the packages does what rpmlint says. Its just fine in this case, no reason to make rpmlint foolish.

- too see what's going on in the build (e.g. to see the gcc flags), please add VERBOSE=1 to make. You can also directly call make -k instead of make MAKE=make -k, don't you (not tried)?:
make -k %{?_smp_mflags} VERBOSE=1

- the examples/ should be simply packaged as %doc too.

- please redirect the output of ./_build/tools/divine-mc help into /dev/null

- there are some prebuilt jars, which must be rebuilt from source or removed. The sources for them are located at http://svn.foldr.org/~michaelw/nips-promela-compiler/trunk/ (according to upstream information), as I doubt they will be useful for any other package in Fedora, I'd suggest adding them as Source1.. Please refer to the Java Guidelines when building them:
https://fedoraproject.org/wiki/Packaging/Java

Comment 7 Milos Jakubicek 2009-03-05 10:47:30 UTC
(In reply to comment #6)

> Moreover you should remove -fomit-frame-pointer (this is prohibited in Fedora,
> it makes debugging harder or impossible) and -pipe+ (gcc doesn't seem to know
> it -- don't know what's the difference to -pipe which is in Fedoras standard
> gcc flags).

Regarding -pipe+: this comes from your sedding:
+ sed -i -e 's/ -gstabs\+//' CMakeLists.txt

Remove the \ before + and it will be ok.

Comment 8 David A. Wheeler 2009-03-09 16:39:26 UTC
I've resolved all the comments above, and I think it's ready to go:
* The patches had already been submitted; the .spec file now includes the link
* gcc flags - exported before ./configure, removed -fomit-frame-pointer
* Let rpmlint whine.
* make VERBOSE=1
* the examples/ should be simply packaged as %doc too.
* No longer use "--help" as a test; there are better tests anyway.
* Rebuilt the prebuilt jars
* Fixed sed to remove -gstabs+
* I didn't add _additional_ tests, but I fully automated checking the test results for the tests I had.

Builds on Fedora 10 and Fedora 11:
http://koji.fedoraproject.org/koji/taskinfo?taskID=1231458
http://koji.fedoraproject.org/koji/taskinfo?taskID=1231988

rpmlint emits one complaint, which is spurious:
 divine-mc.spec:114: W: configure-without-libdir-spec
 0 packages and 1 specfiles checked; 0 errors, 1 warnings.
As noted in the .spec file, this is because the "./configure" program
isn't GNU configure (it's from cmake), so there is no libdir option to invoke.
Therefore, ignore the rpmlint warning from this line.

I think it's ready to go!

Would you approve this, so we can get this into CVS today (and meet the F11 deadline)?

Comment 9 David A. Wheeler 2009-03-09 16:44:01 UTC
Here are the new spec and SRPM files:
http://www.dwheeler.com/divine-mc-1.3-6.fc10.src.rpm
http://www.dwheeler.com/divine-mc.spec

(These versions, posted here, improved the changelog text compared to the one that went through koji scratch builds.  However, I've rebuilt locally using this spec/SRPM, and did rpmlint, so I believe that these are 100% fine.)

Comment 10 Milos Jakubicek 2009-03-09 17:22:11 UTC
David, I'm currently pretty busy and will look at it tomorrow or on Wednesday, but don't worry, the package will be still included in F11 final, just not in the beta.

Comment 11 David A. Wheeler 2009-03-09 17:46:28 UTC
I understand.  Thanks!

Comment 12 David A. Wheeler 2009-03-17 19:52:39 UTC
Milos: Have you had a chance to look at the package?  Any issues remaining (hope not)?

Comment 13 Milos Jakubicek 2009-03-18 09:42:44 UTC
Yes, I had -- sorry for answering late but there were indeed some things I had to clarify with Peter (upstream).

First of all, the install target of cmake doesn't install all the binaries it should -- there should be following files installed into %{_bindir}:

./_build/tools/divine-mc.compile-pml
./_build/tools/divine-mc.combine
./_build/tools/divine-mc
./_build/tools/divine-mc.probabilistic
./_build/tools/divine-mc.simulate

This can be fixed by adding the missing into tools/CMakeLists.txt:install( TARGETS divine-mc divine-mc.simulate DESTINATION bin ).

And now the real problem: I found the official site of Promela, see http://wwwhome.cs.utwente.nl/~michaelw/nips/ (please use the tarball from there as Source1), and as there are several projects using Promela I had to reconsider the decision of including Promela into divine-mc. Moreover, one should quote here what the guidelines say:

"Fedora packages should make every effort to avoid having multiple, separate, upstream projects bundled together in a single package."

Well, unfortunately, this is now impossible. The jars are packed into one perl script (divine-mc.compile-pml) and unpacked runtime. This is hard to bypass without heavy code changes, but Peter agreed on making divine-mc independent on Promela location in 2.0 version (upstream trac ticket placed under http://anna.fi.muni.cz/divine/trac/ticket/14)

Would you agree on packaging Promela too (...I would review it) so that it could be removed from divine-mc 2.0?

To sum it up:

* please fix the cmake install target, make sure that the Perl dependencies are ok then, see: https://fedoraproject.org/wiki/Packaging/Perl#Perl_Requires_and_Provides

* use upstreams tarball URL for Source1 (Promela), please add the link to the trac ticket with the necessary explanation why it is not packaged separate now.

* regarding Java, the BR and R should be versioned, hence please use:

BuildRequires:  java-devel >= 1:1.6.0
BuildRequires:  ant

Requires:       java >= 1:1.6.0
Requires:       jpackage-utils

(BR: jpackage-utils is pulled by ant)

* regarding the following test:

# This one is omitted; it takes too long to be useful as a build test:
# ./_build/tools/divine-mc owcty examples/peterson-liveness.dve

You can surround this one with:

%if %{?_with_tests:1}%{!?_with_tests:0}
./_build/tools/divine-mc owcty examples/peterson-liveness.dve
%endif

so that one can run this test by passing "--with tests" to rpmbuild on demand.

* I would appreciate if you would submit the review request for Promela before approving this package (the package and review shouldn't be problematic AFAIK).

I hope this is all...;)

Comment 14 David A. Wheeler 2009-03-22 14:44:50 UTC
Okay, I've tried to respond to all changes from Comment #13 ; the sole exception is that I didn't version Java (it makes Fedora 10 builds fail, and doesn't seem necessary).  Comments?  First, a discussion of how I handled each comment...

First, thanks for coordinating with upstream!!  I appreciate that.

I've installed all the binaries as you suggested.  I had earlier figured that if they weren't getting installed, they were less mature, but I agree that letting users make the decision of what to run is reasonable.

I'll go package Promela next, so that it can be removed from divine-mc 2.0.  But I don't think Java needs to be versioned; can you help me understand why it must be, before I do that? (I'll use this package as a starting point.)

Regarding: "please fix the cmake install target, make sure that the Perl dependencies are ok then, see:
https://fedoraproject.org/wiki/Packaging/Perl#Perl_Requires_and_Provides " I don't see anything that needs doing.  It doesn't use much of perl, and it's not a perl module.

I switched to the upstreams tarball URL, and added the link to trac ticket on why it's not currently packaged separately.

You said: "regarding Java, the BR and R should be versioned, hence please use:
BuildRequires:  java-devel >= 1:1.6.0 ... 
Requires:       java >= 1:1.6.0"  Versioning Java makes the Fedora 10 build fail, and doesn't seem necessary; 1.5 seems to work just fine.

I surrounded the "take too long" test as suggested.  Very nice!

"I would appreciate if you would submit the review request for Promela before
approving this package (the package and review shouldn't be problematic AFAIK)."  I understand.   But can you explain why you think java and java-devel need to be versioned?

I did rpmlint on the .src.rpm, .spec, and a binary RPM.  The only message is:
"divine-mc.src:134: W: configure-without-libdir-spec"
and as discussed earlier, this is a bogus warning.

I built this with koji on dist-f10 and dist-f11, builds on all architectures:
http://koji.fedoraproject.org/koji/taskinfo?taskID=1252929
  0 free  0 open  5 done  0 failed
http://koji.fedoraproject.org/koji/taskinfo?taskID=1252947
  0 free  0 open  5 done  0 failed

Here's the latest SRPM:
 http://www.dwheeler.com/divine-mc-1.3-7.fc10.src.rpm

Comment 15 Milos Jakubicek 2009-03-27 14:39:29 UTC
(In reply to comment #14)
> You said: "regarding Java, the BR and R should be versioned, hence please use:
> BuildRequires:  java-devel >= 1:1.6.0 ... 
> Requires:       java >= 1:1.6.0"  Versioning Java makes the Fedora 10 build
> fail, and doesn't seem necessary; 1.5 seems to work just fine.

Sorry for the delay.

Well, it probably fails because you've wrong version of java-devel installed. This is because java-devel is just a provides (try `yum provides java-devel`). But anyway, if you tested building on 1.5 and working fine with 1.6, then it is not necessary.

Comment 16 David A. Wheeler 2009-03-28 16:47:57 UTC
Sounds like everything's okay then.  Yes, I did test building on both 1.5 and 1.6.  I did local builds, and then used koji to do builds on F10 and to-be-F11.

Any other comments on this package?

Comment 17 Milos Jakubicek 2009-04-13 14:30:26 UTC
(In reply to comment #16)
> Sounds like everything's okay then.  Yes, I did test building on both 1.5 and
> 1.6.  I did local builds, and then used koji to do builds on F10 and to-be-F11.
> 
> Any other comments on this package?  

No, this seems to be sane -- what about promela? Have you already submitted a review request (couldn't find any)?

Comment 18 Petr Rockai 2009-04-15 22:11:50 UTC
Hi,

I have uploaded divine-mc 1.4 today, that includes an important correctness fix for the nested DFS implementation that's by default used for single-threaded verification runs. Additionally, it improves performance of OWCTY in some cases (the algorithm used for multi-threaded verification).

Unfortunately, I didn't get around to fix the administrative problems you have encountered while working on the package -- mostly the promela jars issue and the incomplete "make install" target. I'll try to make a 1.4.1 release next week that would address those.

Thanks,
   Petr.

Comment 19 David A. Wheeler 2009-04-18 21:48:59 UTC
Petr

Comment 20 David A. Wheeler 2009-04-18 22:04:16 UTC
(Sorry for the blank previous comment.)

Petr: Would you mind "taking over" packaging divine-mc for Fedora?  I feel silly trying to package this program for Fedora when there's a clear expert who could do it much better instead.  Feel free to use my Fedora packaging for divine-mc version 1.3 as a starting point.  If I were you, I'd wait for your divine-mc 1.4.1 release next week, and use that as the baseline.

I haven't submitted a request to package the NIPS Promela compiler yet because my package has mysterious errors that I haven't figured out.  It compiles fine on F10, but not on F11.  On F11 (via koji) its test complains that in the XML, the attribute "line" doesn't have a value... but I looked at the XML and it DOES have a value.  Ugh.   I'm getting an F11 setup so I can track this down, but someone who's more familiar with this program's innards could probably figure this out far faster than I could.  My draft package is here: http://www.dwheeler.com/nips-promela-compiler-1.2.5.20070327-1.fc10.src.rpm

Milos: Can you give me advice?  Should I submit a request for a package review of nips-promela-compiler, even though it doesn't work on F11 yet, in the hopes that someone can help me fix it?  Alternatively, does someone want to take over that package?  My goal is to get these things packaged into Fedora (see http://www.openproofs.org )... if someone else takes over lead, that's fine by me!!

Comment 21 Petr Rockai 2009-09-02 14:03:08 UTC
Hi David,

sorry for taking this long. I am sure I drafted a reply to this bug and lost it somewhere a few months (I guess) back. As for maintaining the package: I am a little too busy to work on this right now. I can offer you co-maintainership to a limited extent, however I am not very fluent with .spec files (it's a few years since I have done any rpm packaging work). I can probably do more on the upstream level, improving the source tarball to meet your packaging needs.

As for administrative issues with divine-mc source tarball, I still haven't gotten around to making a 1.4.1 -- I have the CMakeLists and packjars changes ready in the 2.0 branch, so it'll be a matter of straightforward backport.

Thanks,
   Petr.

Comment 22 Milos Jakubicek 2009-10-25 19:48:34 UTC
David, will you finish this review? If not, please close this ticket.

Comment 23 Petr Rockai 2009-11-19 20:43:47 UTC
Hello!

In the meantime, I have released version 2.0 of DiVinE. It should address the packaging problems you have encountered -- the jar files can be provided externally if needed and so on.

Please consider using this new version instead of DiVinE MC 1.4 for packaging. As for what changed since 1.4, there is a list of changes available at http://divine.fi.muni.cz/page.php?page=whatsnew (the tarball can be gotten at http://divine.fi.muni.cz/page.php?page=download).

Yours,
   Petr.

Comment 24 David A. Wheeler 2009-12-23 17:03:28 UTC
Petr - thanks for releasing version 2.0 of DiVinE.

Comment 25 David A. Wheeler 2010-01-25 03:24:08 UTC
Petr - thanks for reorganizing DiVinE so that the jars are separable.  That makes things far more sensible.

I've posted an RPM spec of "nips-promela-compiler" here:
  https://bugzilla.redhat.com/show_bug.cgi?id=558374
I need a reviewer for that - volunteers highly desired.
The nips-promela-compiler package is a prerequisite for DiVinE (if you want to handle models in Promela, the language of SPIN, which I do).  The idea is to get nips-promela-compiler into the Fedora repository, then update the DiVinE spec to match.


Note You need to log in before you can comment on or make changes to this bug.