Tail pad optimization, cache friendlyness and C++ interrop

via Digitalmars-d digitalmars-d at puremagic.com
Wed Jun 18 12:17:49 PDT 2014


On Wednesday, 18 June 2014 at 15:25:11 UTC, Luís Marques wrote:
> On Wednesday, 18 June 2014 at 06:35:01 UTC, Ola Fosheim Grøstad
> wrote:
>> Not really, you can prove termination for all programs with 3 
>> instructions and 3 bytes of RAM. You can do it for all 
>> programs with 4 instructions and 4 bytes of RAM. You can do it 
>> for all programs with N instructions and N bytes of RAM. You 
>> cannot do it for all TMs since they have unbounded storage.
>>
>> Thus you can prove non-trivial properties such as whether a 
>> functions returns with 1, whether it accepts or rejects the 
>> input '0', etc. It might take a lot of time, but you can do it 
>> in a fixed amount of time. You cannot do it for TMs.
>
> Maybe I missed something in this discussion, but unless you are
> not including jumps/loops in those N instructions, just because
> the number of instructions and memory is bounded does not mean
> you can prove (for arbitrary programs) that the program
> terminates.
>

Jumps and loops don't matter. The point is that such a program 
only has a finite amount of possible states: The 4 bytes of RAM, 
plus the current instruction pointer (to be 2 bits for 4 
instructions). In this case, there are only

     2^(4*8) * 2^2 = 2^34 = 17179869184

different states. If during execution you encounter a state that 
you've already seen before, you know that the program will go 
into an infinite loop. This is easy to implement using a bitmap.

Of course, said bitmap will soon become too large to handle in 
practice if you want to analyze realistic "interesting" programs.


More information about the Digitalmars-d mailing list