Refine, Bisim, Acess I/O error message

ghost commented 7 years ago

Hi All,

I am trying to run the Refine, Bisim, and Access tests in my new installation of Sel4 on a dual boot ubuntu 16.04-1 LTL (Xenial Xerus) . I did not get what the error message means, it is quite short (please see the example below). If someone can help I will appreciate that a lot.

One note: the first time I ran the tests on my dual boot machine the tests were interrupted due to the small Ubuntu partition size (~50 G at that time) the tests Refine, Bisim, and Acess all have been executing at that time and they failed due to lack of memory and nothing was written. Later I expanded the ubuntu partition (to 138 G), all tests- except these three-worked (some skipped due to dependencies). Moreover, when I use: " find $HOME -iname 'Refine.*' -size 0M " it returns : /home/ssrgv/.isabelle/heaps-ARM-home-ssrgv-Desktop-verification-isabelle/polyml-5.6_x86_64-linux/log/Refine.gz

the same happens for Bisim and Access.

Does this mean the size is 0 and probably nothing is written in this file? So there is no input and thus no output? If so can you please advise how to solve it?

Example: :~/Desktop/verification/l4v$ ./isabelle/bin/isabelle build -d . -v -b Refine Started at Tue Dec 20 11:44:16 EST 2016 (polyml-5.6_x86_64-linux on ssrgv-ThinkPad-T440p) ISABELLE_BUILD_OPTIONS=""

ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"

ML_PLATFORM="x86_64-linux" ML_HOME="/home/ssrgv/.isabelle/contrib/polyml-5.6-1/x86_64-linux" ML_SYSTEM="polyml-5.6" ML_OPTIONS="-H 2000"

Session Pure/Pure Session HOL/HOL (main) Session HOL/HOL-Word (main) Session Unsorted/Word_Lib Session Specifications/ASpec Session Proofs/AInvs Session Proofs/BaseRefine Session Proofs/Refine *** I/O error Finished at Tue Dec 20 11:44:19 EST 2016 0:00:03 elapsed time, 0:00:17 cpu time

talsewell commented 7 years ago

I think that Isabelle might not be handling these truncated files.

I know that Isabelle does peek at its old logs to optimise its current runs. It's possible that it doesn't expect a badly formatted gzip archive.

I'd suggest just removing them, especially if their size is 0, and seeing if Isabelle now makes progress.

Cheers, Thomas.

On 21/12/16 04:09, AmerTahat wrote:

Hi All,

I am trying to run the Refine, Bisim, and Access tests in my new installation of Sel4 on a dual boot ubuntu 16.04-1 LTL (Xenial Xerus) . I did not get what the error message means, it is too short (please see the example below). If some one can help I will appreciate that a lot.

One note: the first time I ran the tests on my dual boot machine the tests were interrupted due to the small Ubuntu partition size (~50 G) the tests Refine, Bisim, and Acess all have been executing at that time and they failed due to lack of memory and nothing was written. Later I expanded the ubuntu partition, all tests except these three worked (some skipped due dependencies). Moreover, when I use: " find $HOME -iname 'Refine.*' -size 0M " it returns : /home/ssrgv/.isabelle/heaps-ARM-home-ssrgv-Desktop-verification-isabelle/polyml-5.6_x86_64-linux/log/Refine.gz

the same for Bisim and Access.

Does this mean the size is 0 and probably nothing is written in this file? So there is no input and thus no output? If so can you please advice how to solve it?

Example: :~/Desktop/verification/l4v$ ./isabelle/bin/isabelle build -d . -v -b Refine Started at Tue Dec 20 11:44:16 EST 2016 (polyml-5.6_x86_64-linux on ssrgv-ThinkPad-T440p) ISABELLE_BUILD_OPTIONS=""

ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"

ML_PLATFORM="x86_64-linux" ML_HOME="/home/ssrgv/.isabelle/contrib/polyml-5.6-1/x86_64-linux" ML_SYSTEM="polyml-5.6" ML_OPTIONS="-H 2000"

Session Pure/Pure Session HOL/HOL (main) Session HOL/HOL-Word (main) Session Unsorted/Word_Lib Session Specifications/ASpec Session Proofs/AInvs Session Proofs/BaseRefine Session Proofs/Refine *** I/O error Finished at Tue Dec 20 11:44:19 EST 2016 0:00:03 elapsed time, 0:00:17 cpu time

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/seL4/l4v/issues/15, or mute the threadhttps://github.com/notifications/unsubscribe-auth/ANQQ8PeRHGRinBRoE39hr_eEMZyOBTsfks5rKAvUgaJpZM4LSElu.

ghost commented 7 years ago

Thanks a lot Thomas!

I was considering changing the names of the files i.e renaming the files, but your suggestion is more appropriate since their sizes were 0. Thus, I removed the files from the log then all three tests worked fine. However, one of the tests which was skipped previously " CRefine" -due to dependency -has failed. The message is below and a small question. I do appreciate your advise on how to fix it!

Note: I had run this "CRefine" test independently before I managed to fix Refine test. So I removed it from the log file as well and then I retested it after the fix, but yet it gives the error 137: " Ignoring duplicate rewrite rule". The error message asks to see the log file -please see the full error message below. Thus, when I use zless CRefine, I can see the error "Ignoring duplicate rewrite rule" associated to some files such as:

file=~/Desktop/verification/l4v/proof/crefine/Arch_C.thy^ ~/Desktop/verification/l4v/proof/crefine/Invoke_C.thy

Does this mean that I need to remove/rename crefine from proof directory as well- then retest? It seems like the proofs are corrupted maybe following the first independent building for CRefine? Or does the new sel4 modifications on CRfeine e.g on " Refine_c.thy" led to this? I have seen a comment for example on Refine_c.thy states that ;

" New testfile for graph-refine export with new handling code. Also some slight tweaks to some CRefine proofs that will be needed to remove DONT_TRANSLATE markers from certain key places in the seL4 code. These proofs are also compatible with previous seL4."

Again, I will appreciate your advise!

Thanks in advance.

Error 137:

CRefine: theory Refine_C /home/ssrgv/Desktop/verification/isabelle/lib/scripts/run-polyml-5.6: line 100: 28276 Killed "$POLY" -q -i $ML_OPTIONS CRefine FAILED (see also /home/ssrgv/.isabelle/heaps-ARM-home-ssrgv-Desktop-verification-isabelle/polyml-5.6_x86_64-linux/log/CRefine)

theory "Refine_C"

53.794s elapsed time, 179.736s cpu time, 52.884s GC time

Ignoring duplicate rewrite rule:

seL4_NonArchObjectTypeCount \ 5

Ignoring duplicate rewrite rule:

ccorres_underlying ?sr1 ?\1 ?r1 ?xf1 ?arrel1 ?axf1 ?P1 ?P'1 ?hs1

(liftM ?t1 ?f1) ?g1 \

ccorres_underlying ?sr1 ?\1 (?r1 \ ?t1) ?xf1

(?arrel1 \ ?t1) ?axf1 ?P1 ?P'1 ?hs1 ?f1 ?g1

Bad Simplifier context: renamed bound variable ":001" to ":001a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")

Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")

Bad Simplifier context: renamed bound variable ":001" to ":001a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")

Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")

Bad Simplifier context: renamed bound variable ":001" to ":001a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")

Ignoring duplicate rewrite rule:

objBits ?v \ objBitsKO (injectKO ?v)

Unfinished session(s): CRefine Finished at Wed Dec 21 00:29:28 EST 2016 0:20:48 elapsed time, 1:08:42 cpu time, factor 3.30 ../misc/isa-common.mk:48: recipe for target 'CRefine' failed make: *** [CRefine] Error 137

40/43 tests succeeded. Another two tests were skipped due to dependency.

lsf37 commented 7 years ago

Interesting, the log file seems to have only warnings, no errors, and it looks like the proof part actually finished successfully (theory "Refine_C"'/53.794s elapsed time, 179.736s cpu time, 52.884s GC time).

It's possible that there was not enough RAM for polyml to prepare the image that is written to disk in the end. RAM requirements for CRefine are about 16GB currently, I think. Did the machine have that much available?

lsf37 commented 7 years ago

Looking at our regression test, CRefine without constrained memory finishes with the following:

CRefine passed ( 0:59:44 real, 3:10:32 cpu, 24.34GB)

This means your run probably did not complete the proof (20:48min elapsed time from the log), but memory might indeed be the problem.

The messages "Ignoring duplicate rewrite rule" and "Bad Simplifier context" are warnings and are expected output in the log file. Would you be able to attach the complete log file?

ghost commented 7 years ago

Thanks a lot for your explanation!

Yes, it seems like a memory issue! I checked the system information, the RAM falls short below 16 G. Its installed physical RAM is 16 G, but its total physical RAM is 15.9 G and the usable RAM is 15.6 G. It seems like a small part of the RAM is preserved to the hardware.

To make sure that this lack of memory was the reason, I ran the system monitor application to observe the traffic while running the test. In deed, the point that the monitor reported ~15.6 G used with 99.7% usage of the RAM corresponded to the point it reached Refine_c in the log file. Then the machine became slow for a short while, then the warning message showed up and then the test stopped as can be seen in the attachments.

For the full log please see the attachments: test results logs.zip

Thanks so much for the explanations!

seL4 / l4v