| Bug #45737 | BACKUP: ASSERT failure in stream_v1_transport.c | ||
|---|---|---|---|
| Submitted: | 25 Jun 2009 8:24 | Modified: | 6 Aug 2009 19:45 |
| Reporter: | Jørgen Løland | Email Updates: | |
| Status: | Closed | Impact on me: | |
| Category: | MySQL Server: Backup | Severity: | S3 (Non-critical) |
| Version: | 6.0-backup | OS: | Any |
| Assigned to: | Rafal Somla | CPU Architecture: | Any |
[25 Jun 2009 11:29]
Rafal Somla
Probably duplicate of BUG#44569 - investigating.
[26 Jun 2009 11:59]
Jørgen Løland
WL#4769 depends on this bug.
[9 Jul 2009 9:28]
Rafal Somla
Here is a proof that this assertion could not fail :). In the proofs hdr, pos and end refer to the members of backup_stream::buf structure (s->buf). Lemma 1: After rester_output_buffer() we have hdr = pos < end. ------- Pf: This function sets pos := bgn and end := bgn + block_size. Then, it possibly moves pos few bytes to the right, but after that it still should be less than end, because block_size is bigger. Finally it sets hdr := pos. Thus the post-condition holds at exit time. QED. Lemma 2: After write_buffer() we have hdr = pos < end. -------- Pf: The call to as_write_all() does not matter because it doesn't touch the buffer. Before return, either: a) pos = end: in that case restet_output_buffer() is called and after that post condition holds according to Lemma 1. b) pos < end: then hdr := pos is executed which does not change pos or end and thus hdr = pos < end after that. QED. Lemma 3: If hdr < pos before calling close_current_fragment() then hdr < pos also after the call. ------- Pf: The only place where hdr and pos can be changed is the body of the loop. We prove that hdr < pos is an invariant of this body. If body is entered we know also that pos < end. Note that the body never changes pos because its value is stored in current_fragment.end and pos is restored to that value if changed. Also, biggest_fragment_prefix() does not touch the buffer. hdr is changed in the body only if a non-trivial prefix of the fragment is isolated (i.e., current_fragment.begin < current_fragment.end after a call to bigest_fragment_prefix()). In that case pos is set to point at the end of the prefix and write_buffer() is called after which hdr = pos < end by Lemma 2. Note that write_buffer() does not change pos, thus hdr points now at the first byte of the rest of the fragment (first byte after the prefix). Now pos is restored to the original value which is end of the whole fragment. Thus the remainder of the fragment lies now between bytes pointed by hdr and pos. Since it is not empty, we have hdr < pos (*). This is still the case after --hdr. This proves the invariant and the claim. More detailed proof of (*): After write_buffer, hdr = current_fragmet.begin (the current value of pos). After restoring its original value, pos = current_fragment.end. Since we are within if() bode, we know that hdr < pos. QED. Theorem: Assertion pos < end in bstream_write_part() (stream_v1_transport.c:1087) can not fail. ------- Pf: Assume that the assertion has failed. Note that we could not have pos < end before the call to bstream_flush(), because the if() body will not be executed and the assertion would not fail. It is not possible that pos > end, because pos <= end is a global invariant. This was also checked by additional assertions. Hence bstream_flush() must have been called. Before this call we had bgn < end as otherwise we will exit earlier, at the first return. Hence, by Lemma 3, pos < end after the call to bstream_flush(). This contradicts our assumption that assertion has failed. QED.
[10 Jul 2009 9:21]
Rafal Somla
Hmm, one lemma is missing. Correcting here. Lemma 4: if bgn < pos before calling bstream_flush() then pos < end after the call. ------- Pf: We will not exit at first return because bgn < pos. If we exit at 2nd return then this is after write_buffer(), after which pos < end by Lemma 2. Otherwise we know that hdr < pos and thus after close_current_fragmet() we still have hdr < pos by Lemma 3. If we execute pos++ then still hdr < pos. Since bgn <= hdr < pos, we have bgn < pos and write_buffer() will be called. After that pos < end by Lemma 2. Thus post condition holds at exit. QED. Theorem: Assertion pos < end in bstream_write_part() (stream_v1_transport.c:1087) can not fail. ------- Pf: Assume that the assertion has failed. Note that we could not have pos < end before the call to bstream_flush(), because the if() body will not be executed and the assertion would not fail. It is not possible that pos > end, because pos <= end is a global invariant. This was also checked by additional assertions. Hence bstream_flush() must have been called. Before this call we had bgn < end as otherwise we will exit earlier, at the first return. Hence, by Lemma 4, pos < end after the call to bstream_flush(). This contradicts our assumption that assertion has failed. QED.
[10 Jul 2009 13:00]
Rafal Somla
Patch which adds a unit test which triggers this failure
Attachment: test.diff (application/octet-stream, text), 4.21 KiB.
[13 Jul 2009 14:23]
Rafal Somla
REFINED PROBLEM DESCRIPTION =========================== As the unit test demonstrates, it is possible to arrive at a situation where the output buffer is empty (buf.begin == buf.header == buf.pos) and at the same time is at the very end of the current output block (buf.pos == buf.end). Since buffer is empty (buf.begin == buf.pos) a call to bstream_flush() in bstream_write_part() will do nothing and then the following assetion fails because it is still the case that buf.pos == buf.end. PROPOSED SOLUTION ================= Add code to bstream_flush() which in the above situation resets output buffer so that next output block is entered. That is, ensure post-condition that always buf.pos < buf.end after a call to bstream_flush().
[13 Jul 2009 14:26]
Rafal Somla
The proof above is of course wrong. To be precise, this step in the proof of the main theorem: "Before this call we had bgn < end as otherwise we will exit earlier, at the first return". What was meant is this return statement:
/* return if there is nothing to write */
if (data->begin >= data->end)
return BSTREAM_OK;
But it does not look at s->buf.begin and s->buf.end but rather at an unrelated data->begin and data->end. So that was a stupid confusion.
[13 Jul 2009 15:54]
Ingo Strüwing
I agree with the proposed solution. Is sounds reasonable.
[14 Jul 2009 12:58]
Bugs System
A patch for this bug has been committed. After review, it may be pushed to the relevant source trees for release in the next version. You can access the patch from: http://lists.mysql.com/commits/78646 2846 Rafal Somla 2009-07-14 Bug#45737 - BACKUP: ASSERT failure in stream_v1_transport.c It is possible to arrive at a situation where backup stream's output buffer is empty (buf.begin == buf.header == buf.pos) and at the same time is at the very end of the current output block (buf.pos == buf.end). If bstream_write_part() is called in such situation, it calles bstream_flush() expecting that after that there will be free space in the buffer (buf.pos < buf.end). This is checked with an assertion. Before this fix, bstream_flush() did nothing in the above situation leading to failure of the assertion in bstream_write_part(). After this patch, it will be ensured that after bstream_flush() there always is some free space in the output buffer. @ sql/backup/stream_v1_transport.c Call reset_output_buffer() if it is empty but at the end of the current output block. This will move stream to the next output block and prepare it for accepting more data. @ unittest/backup/bug45737-t.c A unit test which provokes the situation which lead to assertion failure.
[14 Jul 2009 13:27]
Bugs System
A patch for this bug has been committed. After review, it may be pushed to the relevant source trees for release in the next version. You can access the patch from: http://lists.mysql.com/commits/78647 2845 Rafal Somla 2009-07-14 Bug#45737 - BACKUP: ASSERT failure in stream_v1_transport.c It is possible to arrive at a situation where backup stream's output buffer is empty (buf.begin == buf.header == buf.pos) and at the same time is at the very end of the current output block (buf.pos == buf.end). If bstream_write_part() is called in such situation, it calles bstream_flush() expecting that after that there will be free space in the buffer (buf.pos < buf.end). This is checked with an assertion. Before this fix, bstream_flush() did nothing in the above situation leading to failure of the assertion in bstream_write_part(). After this patch, it will be ensured that after bstream_flush() there always is some free space in the output buffer. @ sql/backup/stream_v1_transport.c Call reset_output_buffer() if it is empty but at the end of the current output block. This will move stream to the next output block and prepare it for accepting more data. @ unittest/backup/bug45737-t.c A unit test which provokes the situation which lead to assertion failure.
[14 Jul 2009 16:14]
Ingo Strüwing
Approved. No comments. All looks fine.
[14 Jul 2009 17:25]
Chuck Bell
Changed reviewer to Chuck while Jorgen is on vacation.
[14 Jul 2009 17:25]
Chuck Bell
Changed reviewer to Chuck while Jorgen is on vacation.
[14 Jul 2009 18:15]
Chuck Bell
Approved pending minor changes.
[15 Jul 2009 6:23]
Bugs System
A patch for this bug has been committed. After review, it may be pushed to the relevant source trees for release in the next version. You can access the patch from: http://lists.mysql.com/commits/78698 2846 Rafal Somla 2009-07-15 Bug#45737 - BACKUP: ASSERT failure in stream_v1_transport.c It is possible to arrive at a situation where backup stream's output buffer is empty (buf.begin == buf.header == buf.pos) and at the same time is at the very end of the current output block (buf.pos == buf.end). If bstream_write_part() is called in such situation, it calles bstream_flush() expecting that after that there will be free space in the buffer (buf.pos < buf.end). This is checked with an assertion. Before this fix, bstream_flush() did nothing in the above situation leading to failure of the assertion in bstream_write_part(). After this patch, it will be ensured that after bstream_flush() there always is some free space in the output buffer. @ sql/backup/stream_v1_transport.c Call reset_output_buffer() if it is empty but at the end of the current output block. This will move stream to the next output block and prepare it for accepting more data. @ unittest/backup/bug45737-t.c A unit test which provokes the situation which led to the assertion failure.
[28 Jul 2009 6:34]
Rafal Somla
Has been already pushed to team tree on 2009-07-15, with this merge cset: ingo.struewing@sun.com-20090715090055-ad2xvrgz16y4a3mn
[6 Aug 2009 8:27]
Bugs System
Pushed into 5.4.4-alpha (revid:alik@sun.com-20090806082225-qssc912qdv1mm6xv) (version source revid:ingo.struewing@sun.com-20090715090055-ad2xvrgz16y4a3mn) (merge vers: 5.4.4-alpha) (pib:11)
[6 Aug 2009 19:45]
Paul DuBois
Not in any released version. No changelog entry needed.
[23 Dec 2009 15:50]
Bugs System
A patch for this bug has been committed. After review, it may be pushed to the relevant source trees for release in the next version. You can access the patch from: http://lists.mysql.com/commits/95560 3012 Chuck Bell 2009-12-23 Bug#45737 - BACKUP: ASSERT failure in stream_v1_transport.c It is possible to arrive at a situation where backup stream's output buffer is empty (buf.begin == buf.header == buf.pos) and at the same time is at the very end of the current output block (buf.pos == buf.end). If bstream_write_part() is called in such situation, it calles bstream_flush() expecting that after that there will be free space in the buffer (buf.pos < buf.end). This is checked with an assertion. Before this fix, bstream_flush() did nothing in the above situation leading to failure of the assertion in bstream_write_part(). After this patch, it will be ensured that after bstream_flush() there always is some free space in the output buffer. original changeset: 2599.158.4 @ unittest/backup/bug45737-t.c A unit test which provokes the situation which led to the assertion failure.
Description: After loading the flightstats database, BACKUP of the flightstats gets an assert failure in stream_v1_transport.c:1077. The code that fails is: 1070 if (s->buf.pos == s->buf.end) 1071 { 1072 ret= bstream_flush(s); 1073 if (ret != BSTREAM_OK) 1074 return BSTREAM_ERROR; 1075 } 1076 1077 ASSERT(s->buf.pos < s->buf.end); Inspecting the core file with gdb reveals this: (gdb) p s->buf.pos $1 = (bstream_byte *) 0xbcd7902 "" (gdb) p s->buf.end $2 = (bstream_byte *) 0xbcd7902 "" Rafal suggests that this could be some wrong behavior in bstream_flush; buf.pos==buf.end means that there is no space left in this buf How to repeat: Load the Flightstats database Run BACKUP The flightstats database is too big to attach to this bug report. Suggested fix: Find out why flush does not work properly.