7.6.2.1330 EMPTY-BUFFERS BLOCK EXT

When BLK is non-zero you might be running code from blocks. There is absolutely no reason to prevent your code from essentially marking all your buffers as unused. Unlike some other reputable members of the Forth community, I do make a difference between blocks and buffers. I like to associate a state to each buffer. It is an 'enum' value of sorts:

• UNUSED: there is no established mapping between the buffer and a block.
• MAPPED: a mapping between a block and a buffer has been set up (via a call to BLOCK or LOAD).
• DIRTY: a mapping has been established and the buffer is marked for update to mass storage.

EMPTY-BUFFERS just disables the mapping between buffers and blocks (without flushing them to mass storage).

When BLK is non-zero you might be running code from blocks.

Yes.

There is absolutely no reason to prevent your code from essentially marking all your buffers as unused.

Yes. But the specification should say whether this action is allowed (and what its effects) or not (and effects are unspecified). See also the original question on ForthHub.

A better wording for this ambiguous condition is:

An ambiguous condition exists if EMPTY-BUFFERS is executed when BLK contains a non-zero value.

And on the next iteration an exception should be used (to eliminate this ambiguous condition).

EMPTY-BUFFERS just disables the mapping between buffers and blocks

This is allowed. Also, it is allowed to free the memory of buffers.

The section 3.3.3.5 Input buffers says:

The address and length returned by SOURCE, the string returned by PARSE, and directly computed input-buffer addresses are valid only until the text interpreter does I/O to refill the input buffer or the input source is changed.

(emphasis mine)

On the other hand, LOAD restores the prior input source specification. Consequently, while the input buffer is being interpreted by LOAD, the input source remains the same for every word encountered by the Forth text interpreter in that input buffer, no matter how many blocks are loaded by nested LOAD calls. And while REFILL (or RESTORE-INPUT) has not been executed, the directly computed input-buffer addresses shall be valid, contiguous, and their contents shall be the same for every encountered word in that input buffer.

This requirement can be violate in the following conditions (depending on particular implementations):

1. A block buffer was assigned to a block using BUFFER, then the block buffer was filled by some contents (without marking this block buffer as UPDATEed, intentionally), then LOAD was called for that block. Since a block buffer was already assigned to that block, LOAD will not read the block from mass storage device and just interprets this block buffer (see the request for clarification #180). Then, if this block buffer will be assigned to another block in a nested LOAD, the contents of this input buffer might not be restored.

2. If a block buffer that is the input buffer will be unassigned using EMPTY-BUFFERS (maybe even in a nested LOAD), the block being interpreted might be assigned a different block buffer, and the input-buffer addresses that was computed before that can become invalid, their contents can be modified, or further computed input-buffer addresses will not be contiguous with the previous ones (even if the previous ones are still valid and their contents are unchanged).

All of these edge cases are handled correctly if a block buffer being interpreted is locked from unassigning until its interpretation is complete.

Perhaps this approach could be promoted as a new requirement for systems (see my post in ForthHub). Nowadays, memory limitations are not so restrictive.

Perhaps the section 7.3.2 Block buffer regions removes the guarantees that 3.3.3.5 provides. It says: “If the input source is a block, these restrictions also apply to the address returned by SOURCE”.

The word LOAD is not mentioned among the restrictions. So, it's unclear whether use of LOAD invalidates the address that was returned by SOURCE.

it's unclear whether use of LOAD invalidates the address that was returned by SOURCE

Just for reference: this was discussed in 2019 regarding the addresses returned by BLOCK and BUFFER.