diff mbox series

[FFmpeg-devel] movenc: Get rid of frag_start

Message ID 20210812044212.484900-1-sehuww@mail.scut.edu.cn
State New
Headers show
Series [FFmpeg-devel] movenc: Get rid of frag_start | expand

Checks

Context Check Description
andriy/x86_make success Make finished
andriy/x86_make_fate success Make fate finished
andriy/PPC64_make success Make finished
andriy/PPC64_make_fate success Make fate finished

Commit Message

Hu Weiwen Aug. 12, 2021, 4:42 a.m. UTC
"frag_start" is redundant, and every occurance can be replaced with cluster[0].dts - start_dts

The proof of no behaviour changes: (All line number below is based on commit bff7d662d728)

"frag_start" is read at 4 place (with all possible call stacks):

mov_write_packet
  ...
  mov_flush_fragment
    mov_write_moof_tag
      mov_write_moof_tag_internal
        mov_write_traf_tag
          mov_write_tfxd_tag (#1)
          mov_write_tfdt_tag (#2)
      mov_add_tfra_entries (#3)
      mov_write_sidx_tags
        mov_write_sidx_tag (#4)

mov_write_trailer
  mov_auto_flush_fragment
    mov_flush_fragment
      ... (#1 #2 #3 #4)
  mov_write_sidx_tags
    mov_write_sidx_tag (#4)
  shift_data
    compute_sidx_size
      get_sidx_size
        mov_write_sidx_tags
          mov_write_sidx_tag (#4)

All read happens in "mov_write_trailer" and "mov_write_moof_tag". So we need to prove no behaviour change in these two
functions.

Condition 1: for every track that have "trk->entry == 0", trk->frag_start == trk->track_duration.

Condition 2: for every track that have "trk->entry > 0", trk->frag_start == trk->cluster[0].dts - trk->start_dts.

Definition 1: "Before flush" means just before the invocation of "mov_flush_fragment", except for the auto-flush case in
"mov_write_single_packet", which means before L5934.

Lemma 1: If Condition 1 & 2 is true before flush, Condition 1 & 2 is still true after "mov_flush_fragment" returns.

    Proof:
    No update to the tracks that have "trk->entry == 0" before flushing, so we only consider tracks that have "trk->entry > 0":

    Case 1: !moov_written and moov will be written in this iteration
        trk->entry = 0                                                                    L5366
        trk->frag_start == trk->cluster[0].dts - trk->start_dts                           Lemma condition
        trk->frag_start += trk->start_dts + trk->track_duration - trk->cluster[0].dts;    L5363
        So trk->entry == 0 && trk->frag_start == trk->track_duration
    Case 2: !moov_written and moov will NOT be written in this iteration
        nothing changed
    Case 3: moov_written
        trk->entry = 0                                                                    L5445
        trk->frag_start == trk->cluster[0].dts - trk->start_dts                           Lemma condition
        trk->frag_start += trk->start_dts + trk->track_duration - trk->cluster[0].dts;    L5444
        So trk->entry == 0 && trk->frag_start == trk->track_duration

    Note that trk->track_duration may be updated for the tracks that have "trk->entry > 0" (mov_write_moov_tag will
    update track_duration of "tmcd" track, but it must have 1 entry). But in all case, trk->frag_start is also updated
    to consider the new value.

Lemma 2: If Condition 1 & 2 is true before "ff_mov_write_packet" invocation, Condition 1 & 2 is still true after it returns.

    Proof:
    Only the track corresponding to the pkt is updated, and no update to relevant variables if trk->entry > 0 before invocation.
    So we only need to prove "trk->frag_start == trk->cluster[0].dts - trk->start_dts" after trk->entry increase from 0 to 1.

    Case 1: trk->start_dts == AV_NOPTS_VALUE
        Case 1.1: trk->frag_discont && use_editlist
            trk->cluster[0].dts = pkt->dts        at L5741
            trk->frag_start = pkt->pts            at L5785
            trk->start_dts = pkt->dts - pkt->pts  at L5786
            So trk->frag_start == trk->cluster[0].dts - trk->start_dts
        Case 1.2: trk->frag_discont && !use_editlist
            trk->cluster[0].dts = pkt->dts        at L5741
            trk->frag_start = pkt->dts            at L5790
            trk->start_dts = 0                    at L5791
            So trk->frag_start == trk->cluster[0].dts - trk->start_dts
        Case 1.3: !trk->frag_discont
            trk->cluster[0].dts = pkt->dts        at L5741
            trk->frag_start = 0                   init
            trk->start_dts = pkt->dts             at L5779
            So trk->frag_start == trk->cluster[0].dts - trk->start_dts
    Case 2: trk->start_dts != AV_NOPTS_VALUE
        Case 2.1: trk->frag_discont
            trk->cluster[0].dts = pkt->dts                at L5741
            trk->frag_start = pkt->dts - trk->start_dts   at L5763
            So trk->frag_start == trk->cluster[0].dts - trk->start_dts
        Case 2.2: !trk->frag_discont
            trk->cluster[0].dts = trk->start_dts + trk->track_duration  at L5749
            trk->track_duration == trk->frag_start                      Lemma condition
            So trk->frag_start == trk->cluster[0].dts - trk->start_dts

Lemma 3: Condition 1 & 2 is true in all case before and after "ff_mov_write_packet" invocation, before flush and after
         "mov_flush_fragment" returns.

    Proof: All updates to relevant variable happen either in "ff_mov_write_packet", or during flush. And Condition 1 & 2
           is true initially. So with lemma 1 & 2, we can prove this use induction.

Noticed that all read of "frag_start" only happen in "trk->entry > 0" branch. Now we need to prove Condition 2 is true
before each read.

Because no update to variables relevant to Condition 2 between "before flush" and "mov_write_moof_tag" invocation, we
can conclude Condition 2 is true before every invocation of "mov_write_moof_tag". No behaviour change in
"mov_write_moof_tag" is proved.

In "mov_write_trailer", No update to relevant variables after the last flush and before the invocation of
"mov_write_sidx_tag". So no behaviour change to "mov_write_trailer" is proved.

Q.E.D.

Signed-off-by: Hu Weiwen <sehuww@mail.scut.edu.cn>
---
Hopefully this patch and/or the proof can make the code more clear to future readers.

Thank you for reading this long proof. I'm doing something like this for the first time. Please kindly point it out if
you find anything incorrect or confusing.

 libavformat/movenc.c | 24 ++++--------------------
 libavformat/movenc.h |  1 -
 2 files changed, 4 insertions(+), 21 deletions(-)

--
2.25.1

Comments

Martin Storsjö Aug. 12, 2021, 8:29 p.m. UTC | #1
On Thu, 12 Aug 2021, Hu Weiwen wrote:

> "frag_start" is redundant, and every occurance can be replaced with 
> cluster[0].dts - start_dts

I think I can agree about this, so I think the patch should be fine, 
thanks for taking the time to study it in detail!

My own mental model of the code, having written it this way, is based 
around having this variable, but I guess I can adapt to this change too.

While the change is ok, can we defer pushing it a couple days, in case 
something comes up in my (or your) mind about something we forgot to think 
about?

// Martin
Martin Storsjö Aug. 18, 2021, 10:21 a.m. UTC | #2
On Thu, 12 Aug 2021, Martin Storsjö wrote:

> On Thu, 12 Aug 2021, Hu Weiwen wrote:
>
>> "frag_start" is redundant, and every occurance can be replaced with 
>> cluster[0].dts - start_dts
>
> I think I can agree about this, so I think the patch should be fine, thanks 
> for taking the time to study it in detail!
>
> My own mental model of the code, having written it this way, is based around 
> having this variable, but I guess I can adapt to this change too.
>
> While the change is ok, can we defer pushing it a couple days, in case 
> something comes up in my (or your) mind about something we forgot to think 
> about?

Pushed this now, thanks!

// Martin
diff mbox series

Patch

diff --git a/libavformat/movenc.c b/libavformat/movenc.c
index a460cd9adae..18410c70fa0 100644
--- a/libavformat/movenc.c
+++ b/libavformat/movenc.c
@@ -4483,8 +4483,7 @@  static int mov_write_tfxd_tag(AVIOContext *pb, MOVTrack *track)
     avio_write(pb, uuid, sizeof(uuid));
     avio_w8(pb, 1);
     avio_wb24(pb, 0);
-    avio_wb64(pb, track->start_dts + track->frag_start +
-                  track->cluster[0].cts);
+    avio_wb64(pb, track->cluster[0].dts + track->cluster[0].cts);
     avio_wb64(pb, track->end_pts -
                   (track->cluster[0].dts + track->cluster[0].cts));

@@ -4563,8 +4562,7 @@  static int mov_add_tfra_entries(AVIOContext *pb, MOVMuxContext *mov, int tracks,
         info->size     = size;
         // Try to recreate the original pts for the first packet
         // from the fields we have stored
-        info->time     = track->start_dts + track->frag_start +
-                         track->cluster[0].cts;
+        info->time     = track->cluster[0].dts + track->cluster[0].cts;
         info->duration = track->end_pts -
                          (track->cluster[0].dts + track->cluster[0].cts);
         // If the pts is less than zero, we will have trimmed
@@ -4602,7 +4600,7 @@  static int mov_write_tfdt_tag(AVIOContext *pb, MOVTrack *track)
     ffio_wfourcc(pb, "tfdt");
     avio_w8(pb, 1); /* version */
     avio_wb24(pb, 0);
-    avio_wb64(pb, track->frag_start);
+    avio_wb64(pb, track->cluster[0].dts - track->start_dts);
     return update_size(pb, pos);
 }

@@ -4679,8 +4677,7 @@  static int mov_write_sidx_tag(AVIOContext *pb,

     if (track->entry) {
         entries = 1;
-        presentation_time = track->start_dts + track->frag_start +
-                            track->cluster[0].cts;
+        presentation_time = track->cluster[0].dts + track->cluster[0].cts;
         duration = track->end_pts -
                    (track->cluster[0].dts + track->cluster[0].cts);
         starts_with_SAP = track->cluster[0].flags & MOV_SYNC_SAMPLE;
@@ -5359,10 +5356,6 @@  static int mov_flush_fragment(AVFormatContext *s, int force)
         mov->moov_written = 1;
         mov->mdat_size = 0;
         for (i = 0; i < mov->nb_streams; i++) {
-            if (mov->tracks[i].entry)
-                mov->tracks[i].frag_start += mov->tracks[i].start_dts +
-                                             mov->tracks[i].track_duration -
-                                             mov->tracks[i].cluster[0].dts;
             mov->tracks[i].entry = 0;
             mov->tracks[i].end_reliable = 0;
         }
@@ -5416,11 +5409,7 @@  static int mov_flush_fragment(AVFormatContext *s, int force)
         MOVTrack *track = &mov->tracks[i];
         int buf_size, write_moof = 1, moof_tracks = -1;
         uint8_t *buf;
-        int64_t duration = 0;

-        if (track->entry)
-            duration = track->start_dts + track->track_duration -
-                       track->cluster[0].dts;
         if (mov->flags & FF_MOV_FLAG_SEPARATE_MOOF) {
             if (!track->entry)
                 continue;
@@ -5440,8 +5429,6 @@  static int mov_flush_fragment(AVFormatContext *s, int force)
             ffio_wfourcc(s->pb, "mdat");
         }

-        if (track->entry)
-            track->frag_start += duration;
         track->entry = 0;
         track->entries_flushed = 0;
         track->end_reliable = 0;
@@ -5760,7 +5747,6 @@  int ff_mov_write_packet(AVFormatContext *s, AVPacket *pkt)
             /* New fragment, but discontinuous from previous fragments.
              * Pretend the duration sum of the earlier fragments is
              * pkt->dts - trk->start_dts. */
-            trk->frag_start = pkt->dts - trk->start_dts;
             trk->end_pts = AV_NOPTS_VALUE;
             trk->frag_discont = 0;
         }
@@ -5782,12 +5768,10 @@  int ff_mov_write_packet(AVFormatContext *s, AVPacket *pkt)
                 /* Pretend the whole stream started at pts=0, with earlier fragments
                  * already written. If the stream started at pts=0, the duration sum
                  * of earlier fragments would have been pkt->pts. */
-                trk->frag_start = pkt->pts;
                 trk->start_dts  = pkt->dts - pkt->pts;
             } else {
                 /* Pretend the whole stream started at dts=0, with earlier fragments
                  * already written, with a duration summing up to pkt->dts. */
-                trk->frag_start = pkt->dts;
                 trk->start_dts  = 0;
             }
             trk->frag_discont = 0;
diff --git a/libavformat/movenc.h b/libavformat/movenc.h
index af1ea0bce64..daeaad1cc68 100644
--- a/libavformat/movenc.h
+++ b/libavformat/movenc.h
@@ -138,7 +138,6 @@  typedef struct MOVTrack {

     AVIOContext *mdat_buf;
     int64_t     data_offset;
-    int64_t     frag_start;
     int         frag_discont;
     int         entries_flushed;