From: Paolo Bonzini <pbonzini@redhat.com>
To: Alex Horn <alex.horn@cs.ox.ac.uk>
Cc: Thomas Melham <tom.melham@balliol.ox.ac.uk>,
qemu-devel@nongnu.org,
Daniel Kroening <Daniel.Kroening@cs.ox.ac.uk>,
Bug 1080086 <1080086@bugs.launchpad.net>
Subject: Re: [Qemu-devel] [Bug 1080086] Re: MC146818 RTC breaks when SET bit in Register B is on.
Date: Mon, 19 Nov 2012 12:42:23 +0100 [thread overview]
Message-ID: <50AA1B1F.5090705@redhat.com> (raw)
In-Reply-To: <CAN1LFUPnfc17n2pv34JBKRBJNMtkzm13Rq4iUCi62dCGqCwmUg@mail.gmail.com>
Il 19/11/2012 12:34, Alex Horn ha scritto:
>> [...] the patch is almost good for inclusion. I'd ask for two changes:
>> 1) please test == 0, not != REG_B_SET;
>> 2) please leave the fuzzicsng test last
>
> I have attached a new patch with the requested changes.
>
> This patch also improves the quality of the functional test by
> checking that RTC_SECONDS is equal (==) to the previously written data
> provided the SET flag in Register B is still enabled. This is
> justified by the data sheet which states that an enabled SET bit
> "stops an existing update" and prevents "a new one from occurring" [1,
> p. 15]. In contrast, once the SET flag is disabled, the RTC_SECONDS
> check uses an inequality (>=) as in the original test case.
Right.
> Out of curiosity, does anyone know how long this particular bug has
> been undetected or how/when it was introduced?
Probably it was introduced last September when the model was rewritten.
But it's really unlikely that the bug would have been detected.
On the other hand, the bug in commit b6db4ac (which also includes a
qtest) was detected by autotest. Could your tool find it, too?
> This could help me explain to others my research interest in symbolic
> execution of hardware models and its application in form of automated
> test generation.
Very interesting (at least to me :)).
> Finally, if there is interest to improve the robustness of the RTC
> model, I could send a patch with several verification conditions (i.e.
> assertions) which can help to expose these kind of bugs in the RTC
> hardware model.
Sure, that's welcome.
In particular, I assume you verified the "next alarm" code to be correct? :)
Paolo
> Recall that most compiler can usually optimize these
> assertions away unless a developer explicitly enables them. They also
> serve as unambiguous code documentation.
>
> With best regards,
> Alex
>
> [1] http://www.freescale.com/files/microcontrollers/doc/data_sheet/MC146818.pdf
>
> On 18 November 2012 08:52, Paolo Bonzini <pbonzini@redhat.com> wrote:
>> Il 17/11/2012 19:47, Alex Horn ha scritto:
>>> I have attached a patch for the most recent version of the file
>>> hw/mc146818rtc.c [1]. The patch also features a functional test which
>>> executes through the QTest framework.
>>>
>>> I would appreciate your thoughts on this.
>>>
>>> [1]
>>> http://git.qemu.org/?p=qemu.git;a=blob;f=hw/mc146818rtc.c;h=98839f278d93452d071054e2a017b3d909b45ab2;hb=9cb535fe4ef08b01e583ec955767a0899ff79afe#l563
>>>
>>> ** Patch added: "register_b_set_flag.patch"
>>> https://bugs.launchpad.net/qemu/+bug/1080086/+attachment/3436808/+files/register_b_set_flag.patch
>>>
>>
>> Hi Alex, the patch is almost good for inclusion. I'd ask for two
>> changes: 1) please test == 0, not != REG_B_SET; 2) please leave the
>> fuzzing test last, because it may leave some registers in an undefined
>> state.
>>
>> Paolo
next prev parent reply other threads:[~2012-11-19 11:42 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-11-17 14:41 [Qemu-devel] [Bug 1080086] [NEW] MC146818 RTC breaks when SET bit in Register B is on Alex Horn
2012-11-17 18:47 ` [Qemu-devel] [Bug 1080086] " Alex Horn
2012-11-18 8:52 ` Paolo Bonzini
2012-11-19 11:34 ` Alex Horn
2012-11-19 11:42 ` Paolo Bonzini [this message]
2012-11-19 14:14 ` Alex Horn
2012-11-19 11:44 ` Paolo Bonzini
2012-11-19 12:12 ` Alex Horn
2012-11-19 12:42 ` Alex Horn
2017-11-07 18:42 ` Peter Maydell
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=50AA1B1F.5090705@redhat.com \
--to=pbonzini@redhat.com \
--cc=1080086@bugs.launchpad.net \
--cc=Daniel.Kroening@cs.ox.ac.uk \
--cc=alex.horn@cs.ox.ac.uk \
--cc=qemu-devel@nongnu.org \
--cc=tom.melham@balliol.ox.ac.uk \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).