8000 alarm: create `ms_to_ticks` helper function by Samir-Rashid · Pull Request #434 · tock/libtock-c · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

alarm: create ms_to_ticks helper function #434

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Jun 7, 2024
Merged

alarm: create ms_to_ticks helper function #434

merged 2 commits into from
Jun 7, 2024

Conversation

Samir-Rashid
Copy link
Contributor
@Samir-Rashid Samir-Rashid commented May 28, 2024 •
edited
Loading

#395 has stalled as the PR has grown beyond original scope. This PR splits out the modifications to arithmetic logic and should get merged before #395.

This mega-size comment was originally in the code explaining the logic of the code change.

static uint32_t ms_to_ticks(uint32_t ms) {
  uint32_t frequency;
  libtock_alarm_command_get_frequency(&frequency);

  // Note the following code is mathematically equivalent to the following
  // more readable conversion.
  // ```
  //   uint32_t seconds         = ms / 1000;
  //   uint32_t leftover_millis = ms % 1000;
  //   uint32_t millihertz      = frequency / 1000; // ticks per millisecond
  //   return (seconds * frequency) + (leftover_millis * millihertz);
  // ```
  // We can check the logical correctness of this conversion by doing dimensional
  // analysis of the units.
  // For the first half, `seconds` (sec) * `frequency` (ticks per second) = a quantity in ticks.
  // And for the second half, `leftover_millis` (milliseconds) * `millihertz` (ticks per millisecond)
  // = a quantity in ticks.
  // Thus, we know the calculation is logically correct as the units cancel out to return ticks.
  //
  // Although these are logically equivalent, this human readable implementation is
  // faulty. I will prove this by (1.) showing an upper bound on the error of this conversion,
  // and then (2.) explaining why this commented human readable implementation is
  // equivalent to the true implementation.
  //
  // Part 1:
  // The splitting of the input milliseconds has no error.
  uint32_t seconds         = ms / 1000;
  uint32_t leftover_millis = ms % 1000;
  // In other words, `seconds` + `leftover_millis` is always == `ms`.

  // The first half of the output converts the seconds component to ticks with no error.
  // This multiplication has no error because the board frequency is given in Hertz (ticks per second).
  uint64_t ticks = (uint64_t) seconds * frequency;

  
8000
// Now that we have converted the full seconds part of `ms` to ticks, we must
  // convert the `leftover_millis`.
  // The only error introduced is by the division step. Division loses
  // all fractional components, so you lose 3 decimal significant figures by doing the division.
  // This does not matter as the remainder lost to integer division is a fraction of a
  // millisecond. It is especially important that this conversion is lower than the
  // true value of the conversion. In summary, the error in `ms_to_ticks` is from losing
  // significant figures, but this loss is less than 1 millisecond of error.
  //
  // Note that the division happens after the multiplication. Let us take a look at a
  // concrete example of a worst case conversion.
  // For a board with an oscillator frequency of 32,768Hz (NRF52840dk), observe the
  // error introduced by arithmetic in the "human readable" implementation of this
  // same line of the code:
  //   uint32_t millihertz      = frequency / 1000; // ticks per millisecond
  //   ticks += leftover_millis * millihertz;
  //
  //   // The worst case is when the remainder `leftover_millis` is `frequency` - 1
  //   ticks += 32767 * millihertz;
  // But what is the value of millihertz here? It is `32768 / 1000` = `32`! This is
  // 2.4% error, has only 2 significant figures, and, worst of all, the division causes the
  // denominator to be smaller than it should be. Dividing by a smaller number causes the
  // entire value of `ticks` to be an overestimate. This is a critical correctness issue.
  // Let's trace an example execution of calculating overflows in `timer_in`. The code uses
  // this line to calculate how many overflows are needed.
  //     const uint32_t max_ticks_in_ms = ticks_to_ms(MAX_TICKS);
  // If `ticks_to_ms` is an overestimate, then a timer set for slightly longer than the
  // true value of `MAX_VALUE` in ms will cause the check for `length of timer` <
  // `max_ticks_in_ms` to be true. This incorrect check will set an overflowed timer and fire
  // too early.
  uint32_t milliseconds_per_second = 1000;
  ticks += ((uint64_t) leftover_millis * frequency) / milliseconds_per_second;

  // Part 2:
  // The human readable and actual implementation are logically equivalent.
  // The only difference is the location of the division by 1000.
  //   leftover_millis * millihertz = leftover_millis * (frequency / 1000)
  //   = leftover_millis * frequency / 1000 = (leftover_millis * frequency) / 1000
  // Thus, by a series of equivalences, these are doing the same calculation.

  return ticks;
}

@Samir-Rashid Samir-Rashid force-pushed the add-ms-to-ticks branch 2 times, most recently from f6d9cc8 to 35b77cd Compare May 28, 2024 21:00
tyler-potyondy
tyler-potyondy requested changes May 28, 2024
View reviewed changes
libtock/services/alarm.c Outdated
Comment on lines 26 to 33
// Note the following code is mathematically equivalent to the following
// more readable conversion.
// ```
// uint32_t seconds = ms / 1000;
// uint32_t leftover_millis = ms % 1000;
// uint32_t millihertz = frequency / 1000; // ticks per millisecond
// return (seconds * frequency) + (leftover_millis * millihertz);
// ```
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that with the exception of this comment, the other lengthy comments/proof in this function should be moved to the PR description.

You can leave a pointer to this PR for those interested in the more in depth discussion you provide here. Having the lengthy description is helpful for future work, but I think more verbose than necessary in the code base. Leaving this for posterity in the PR that is pointed to from the comment seems to offer a good middle ground.

Copy link
Contributor Author
@Samir-Rashid Samir-Rashid May 30, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good idea. I've changed it, and I am pasting the content here temporarily and will move it to the PR description later.

tyler-potyondy
tyler-potyondy requested changes May 31, 2024
View reviewed changes
@tyler-potyondy
Copy link
Contributor

Once you update the comment, rebase on master, and format to pass CI (run make in libtock-c directory) this should be good to go!

bradjc
bradjc previously approved these changes Jun 5, 2024
View reviewed changes
@Samir-Rashid
alarm: create ms_to_ticks helper function
dfa81c6 
This helper function has been thoroughly debugged in tock#395. Floating
point imprecision was causing timer overflows to work incorrectly.
`ms_to_ticks` now better corresponds with the behavior of the
libtock-c 32-bit tick rollover and is precise to 1ms of error.
@Samir-Rashid
alarm: use 64 bits for intermediate tick conversion
fea5e92
@ppannuto ppannuto added this pull request to the merge queue Jun 7, 2024
Merged via the queue into tock:master with commit 2418e1b Jun 7, 2024
2 checks passed
lschuermann
lschuermann reviewed Jun 17, 2024
View reviewed changes
libtock/services/alarm.c
Comment on lines +23 to +33
// This conversion has a max error of 1ms.
// View the justification here https://github.com/tock/libtock-c/pull/434
uint32_t frequency;
libtock_alarm_command_get_frequency(&frequency);

uint32_t seconds = ms / 1000;
uint32_t leftover_millis = ms % 1000;
uint32_t milliseconds_per_second = 1000;

uint64_t ticks = (uint64_t) seconds * frequency;
ticks += ((uint64_t) leftover_millis * frequency) / milliseconds_per_second;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm just catching up to speed, but given that we're in 64-bit arithmetic now, why is this still dealing with seconds and fractional seconds individually? Wouldn't this suffice now?

    ms = (ticks * milliseconds_per_second) / freq
    ticks = (ms * freq) / milliseconds_per_second

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lschuermann lschuermann lschuermann left review comments

@ppannuto ppannuto ppannuto approved these changes

@bradjc bradjc bradjc approved these changes

@tyler-potyondy tyler-potyondy tyler-potyondy approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@Samir-Rashid @tyler-potyondy @ppannuto @bradjc @lschuermann
0