RFR: 8282365: Consolidate and improve division by constant idealizations [v33]

[Quan Anh Mai]

On Mon, 30 Oct 2023 14:13:50 GMT, Raffaello Giulietti <rgiulietti at openjdk.org> wrote:

>> Quan Anh Mai has updated the pull request with a new target base due to a merge or a rebase. The pull request now contains 74 commits:
>> 
>>  - fix proof
>>  - Merge branch 'master' into unsignedDiv
>>  - fix assert macro, benchmarks
>>  - comment styles
>>  - disable test with Xcomp
>>  - remove verify
>>  - fix x86 test
>>  - more rigorous control
>>  - verify the effectiveness of test
>>  - require x64
>>  - ... and 64 more: https://git.openjdk.org/jdk/compare/5224e979...529bd0f9
>
> In the more general case where you know that $|x| \le K$, where $K$ is any positive real number, you would determine $m$ and $c$ as
> 
> $$m = \lceil\log_2 (K d)\rceil = \lceil\log_2 K + \log_2 d\rceil, \qquad c = \lceil 2^m / d\rceil$$

@rgiulietti Yes that is a valid solution, but maybe not the optimal one, which is why trying to find `c` with different values of `m` is necessary.

-------------

PR Comment: https://git.openjdk.org/jdk/pull/9947#issuecomment-1785476105