8237514: Spec Clarification - ByteBuffer::alignmentOffset Spec

Reviewed-by: alanb, psandoz
This commit is contained in:
Brian Burkhalter 2020-01-31 08:04:11 -08:00
parent 953fbd2e66
commit 7db8a1762f
4 changed files with 75 additions and 8 deletions

View File

@ -1871,19 +1871,20 @@ public abstract class $Type$Buffer
* Returns the memory address, pointing to the byte at the given index,
* modulo the given unit size.
*
* <p> The return value is non-negative, with {@code 0} indicating that the
* address of the byte at the index is aligned for the unit size, and a
* positive value that the address is misaligned for the unit size. If the
* address of the byte at the index is misaligned, the return value
* <p> The return value is non-negative in the range of {@code 0}
* (inclusive) up to {@code unitSize} (exclusive), with zero indicating
* that the address of the byte at the index is aligned for the unit size,
* and a positive value that the address is misaligned for the unit size.
* If the address of the byte at the index is misaligned, the return value
* represents how much the index should be adjusted to locate a byte at an
* aligned address. Specifically, the index should either be decremented by
* the return value, or incremented by the unit size minus the return value.
* Therefore given
* the return value if the latter is not greater than {@code index}, or be
* incremented by the unit size minus the return value. Therefore given
* <blockquote><pre>
* int value = alignmentOffset(index, unitSize)</pre></blockquote>
* then the identities
* <blockquote><pre>
* alignmentOffset(index - value, unitSize) == 0</pre></blockquote>
* alignmentOffset(index - value, unitSize) == 0, value &le; index</pre></blockquote>
* and
* <blockquote><pre>
* alignmentOffset(index + (unitSize - value), unitSize) == 0</pre></blockquote>

View File

@ -39,6 +39,7 @@ import java.nio.*;
import java.nio.channels.FileChannel;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.Random;
#end[byte]
@ -492,6 +493,38 @@ public class Basic$Type$
} catch (IOException e) {
throw new UncheckedIOException(e);
}
// alignment identities
final int maxPow2 = 12;
ByteBuffer bb = ByteBuffer.allocateDirect(1 << maxPow2); // cap 4096
Random rnd = new Random();
long seed = rnd.nextLong();
rnd = new Random(seed);
for (int i = 0; i < 100; i++) {
// 1 == 2^0 <= unitSize == 2^k <= bb.capacity()/2
int unitSize = 1 << rnd.nextInt(maxPow2);
// 0 <= index < 2*unitSize
int index = rnd.nextInt(unitSize << 1);
int value = bb.alignmentOffset(index, unitSize);
try {
if (value < 0 || value >= unitSize) {
throw new RuntimeException(value + " < 0 || " +
value + " >= " + unitSize);
}
if (value <= index &&
bb.alignmentOffset(index - value, unitSize) != 0)
throw new RuntimeException("Identity 1");
if (bb.alignmentOffset(index + (unitSize - value),
unitSize) != 0)
throw new RuntimeException("Identity 2");
} catch (RuntimeException re) {
System.err.format("seed %d, index %d, unitSize %d, value %d%n",
seed, index, unitSize, value);
throw re;
}
}
}
private static MappedByteBuffer[] mappedBuffers() throws IOException {

View File

@ -26,7 +26,7 @@
* @bug 4413135 4414911 4416536 4416562 4418782 4471053 4472779 4490253 4523725
* 4526177 4463011 4660660 4661219 4663521 4782970 4804304 4938424 5029431
* 5071718 6231529 6221101 6234263 6535542 6591971 6593946 6795561 7190219
* 7199551 8065556 8149469 8230665
* 7199551 8065556 8149469 8230665 8237514
* @modules java.base/java.nio:open
* java.base/jdk.internal.misc
* @author Mark Reinhold

View File

@ -39,6 +39,7 @@ import java.nio.*;
import java.nio.channels.FileChannel;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.Random;
@ -492,6 +493,38 @@ public class BasicByte
} catch (IOException e) {
throw new UncheckedIOException(e);
}
// alignment identities
final int maxPow2 = 12;
ByteBuffer bb = ByteBuffer.allocateDirect(1 << maxPow2); // cap 4096
Random rnd = new Random();
long seed = rnd.nextLong();
rnd = new Random(seed);
for (int i = 0; i < 100; i++) {
// 1 == 2^0 <= unitSize == 2^k <= bb.capacity()/2
int unitSize = 1 << rnd.nextInt(maxPow2);
// 0 <= index < 2*unitSize
int index = rnd.nextInt(unitSize << 1);
int value = bb.alignmentOffset(index, unitSize);
try {
if (value < 0 || value >= unitSize) {
throw new RuntimeException(value + " < 0 || " +
value + " >= " + unitSize);
}
if (value <= index &&
bb.alignmentOffset(index - value, unitSize) != 0)
throw new RuntimeException("Identity 1");
if (bb.alignmentOffset(index + (unitSize - value),
unitSize) != 0)
throw new RuntimeException("Identity 2");
} catch (RuntimeException re) {
System.err.format("seed %d, index %d, unitSize %d, value %d%n",
seed, index, unitSize, value);
throw re;
}
}
}
private static MappedByteBuffer[] mappedBuffers() throws IOException {