Sequentially constructive model of computation
View Patent ↗System and method for validating a program under a specified model of computation. The model of computation may be related to the synchronous statechart model of computation. A program may be received that specifies a plurality of operations using a variable within a logical tick such that the variable has multiple values within the logical tick. The program may be statically analyzed according to a specified model of computation that specifies program execution based on logical ticks, which may include determining that the program has deterministic semantics that specify deterministic results for each logical tick during execution of the program, including specifying deterministic results of the plurality of operations performed within the logical tick. The program may be validated in accordance with the specified model of computation in response to the determining.
1. A non-transitory computer-readable storage medium having instructions stored thereon that are executable by a computing device to perform operations comprising:
receiving a program that specifies relative sequencing of a first plurality of operations within a logical tick and does not specify relative sequencing of a second plurality of operations within the logical tick, wherein all computations within the logical tick are interpreted as being instantaneous, and wherein logical ticks specify the resolution of functional synchronization for execution of the program;
statically analyzing the program according to a specified model of computation that specifies synchronous program execution based on logical ticks, wherein said statically analyzing the program includes:
determining that the first plurality of operations preserves deterministic execution within the logical tick based on sequence information, wherein deterministic execution comprises a final result of the first plurality of operations within the logical tick; and
determining that the second plurality of operations meets a set of criteria for a deterministic result regardless of ordering, wherein the set of criteria includes one or more of:
a criterion that reads of a variable follow assignments to the variable, unless it is determined that ordering of the reads and assignments is not required for deterministic semantics:
a criterion that at most one absolute assignment is performed for a given variable;
a criterion that assignment operations to a given variable are commutative and associative; or
a criterion that assignment operations to a given variable are of a same type;
wherein one or more of the first plurality of operations do not meet one or more criteria of the set of criteria;
validating the program in accordance with the specified model of computation based on said statically analyzing; and
transforming the program to generate deterministically executable code; and
performing one of:
executing the deterministically executable code using hardware; or
implementing the deterministically executable code in hardware.
2. The non-transitory computer-readable storage medium of claim 1 , wherein the specified model of computation is a sequential model of computation.
3. The non-transitory computer-readable storage medium of claim 1 , wherein the first plurality of operations specify that a variable has multiple values within the logical tick.
4. The non-transitory computer-readable storage medium of claim 1 , wherein the first plurality of operations includes a read operation for a given variable and an assignment operation for the given variable and wherein the sequence information specifies that the read operation occurs before the assignment operation.
5. The non-transitory computer-readable storage medium of claim 1 , wherein the program includes a statechart.
6. A method, comprising:
receiving, by a computing device, a program that specifies relative sequencing of a first plurality of operations within a logical tick and does not specify relative sequencing of a second plurality of operations within the logical tick, wherein all computations within the logical tick are interpreted as being instantaneous, and wherein logical ticks specify the resolution of functional synchronization for execution of the program;
the computing device statically analyzing the program according to a specified model of computation that specifies synchronous program execution based on logical ticks, wherein said statically analyzing the program includes:
determining that the first plurality of operations preserves deterministic execution within the logical tick based on sequence information, wherein deterministic execution comprises a final result of the first plurality of operations within the logical tick; and
determining that the second plurality of operations meets a set of criteria for a deterministic result regardless of ordering;
wherein one or more of the first plurality of operations do not meet one or more criteria of the set of criteria, wherein the set of criteria includes one or more of:
a criterion that reads of a variable follow assignments to the variable, unless it is determined that ordering of the reads and assignments is not required for deterministic semantics:
a criterion that at most one absolute assignment is performed for a given variable;
a criterion that assignment operations to a given variable are commutative and associative; or
a criterion that assignment operations to a given variable are of a same type;
the computing device validating the program in accordance with the specified model of computation based on said statically analyzing; and
the computing device transforming the program to produce deterministically executable output code; and
the computing device performing one of:
executing the deterministically executable code using hardware; or
implementing the deterministically executable code in hardware.
7. The method of claim 6 , wherein the specified model of computation is a sequential model of computation.
8. The method of claim 6 , wherein the first plurality of operations specify that a variable has multiple values within the logical tick.
9. The method of claim 6 , wherein the first plurality of operations includes a read operation for a given variable and an assignment operation for the given variable and wherein the sequence information specifies that the read operation occurs before the assignment operation.
10. The method of claim 6 , wherein the program includes a statechart.
11. An apparatus, comprising:
one or more processing elements; and
one or more memories having program instructions stored thereon that are executable by the one or more processing elements to:
receive a program that specifies relative sequencing of a first plurality of operations within a logical tick and does not specify relative sequencing of a second plurality of operations within the logical tick, wherein all computations within the logical tick are interpreted as being instantaneous, and wherein logical ticks specify the resolution of functional synchronization for execution of the program;
statically analyze the program according to a specified model of computation that specifies synchronous program execution based on logical ticks, including to:
determine that the first plurality of operations preserves deterministic execution within the logical tick based on sequence information, wherein deterministic execution comprises a final result of the first plurality of operations within the logical tick; and
determine that the second plurality of operations meets a set of criteria for a deterministic result regardless of ordering;
wherein one or more of the first plurality of operations do not meet one or more criteria of the set of criteria, wherein the set of criteria includes one or more of:
a criterion that reads of a variable follow assignments to the variable, unless it is determined that ordering of the reads and assignments is not required for deterministic semantics:
a criterion that at most one absolute assignment is performed for a given variable;
a criterion that assignment operations to a given variable are commutative and associative; or
a criterion that assignment operations to a given variable are of a same type;
validate the program in accordance with the specified model of computation based on said statically analyzing; and
transform the program to produce deterministically executable output code; and
perform one of:
executing the deterministically executable code using hardware; or
implementing the deterministically executable code in hardware.
12. The apparatus of claim 11 , wherein the specified model of computation is a sequential model of computation.
13. The apparatus of claim 11 , wherein the first plurality of operations specify that a variable has multiple values within the logical tick.
14. The apparatus of claim 11 , wherein the first plurality of operations includes a read operation for a given variable and an assignment operation for the given variable and wherein the sequence information specifies that the read operation occurs before the assignment operation.