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. Such techniques may allow validation of a larger set of programs than conventional models while maintaining deterministic results.
1. A computer-implemented method, comprising:
utilizing a computing system to perform:
receiving a program, wherein the program specifies a plurality of operations using a variable within a logical tick such that the variable has multiple values within the logical tick;
statically analyzing the program according to a specified model of computation that specifies program execution based on logical ticks, wherein said statically analyzing the program includes:
determining that the program has deterministic semantics, wherein the deterministic semantics 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;
wherein the deterministic semantics is based on, within a given logical tick:
a scheduling of operations that are sequential with respect to each other as specified by the program according to the specified sequence; and
a scheduling of operations that are concurrent with each other such that assignments to a variable are performed before reads of the variable, including scheduling the assignment operations to the variable that are concurrent with each other such that a first assignment operation is scheduled before one or more other assignment operations, wherein the order of the one or more other assignment operations does not influence a final result of the variable for the logical tick; and
validating the program in accordance with the specified model of computation in response to said determining.
2. The method of claim 1 , further comprising compiling the program to produce output code that is deterministically executable.
3. The method of claim 1 , wherein said determining that the program has deterministic semantics is based on sequencing information specified by the program for at least a portion of the plurality of operations.
4. The method of claim 3 , wherein the program explicitly specifies the sequencing information.
5. The method of claim 3 , wherein the at least a portion of the plurality of operations do not specify a deterministic result without the sequencing information.
6. The method of claim 1 , wherein plurality of operations include a read of the variable before an absolute assignment to the variable.
7. A computer system comprising:
one or more processors; and
memory storing program instructions, wherein the program instructions are executable by the one or more processors to cause the computer system to perform operations including:
receiving a program, wherein the program specifies a plurality of operations using a variable within a logical tick such that the variable has multiple values within the logical tick;
statically analyzing the program according to a specified model of computation that specifies program execution based on logical ticks, wherein said statically analyzing the program includes:
determining that the program has deterministic semantics, wherein the deterministic semantics 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;
wherein the deterministic semantics is based on, within a given logical tick:
a scheduling of operations that are sequential with respect to each other as specified by the program according to the specified sequence; and
a scheduling of operations that are concurrent with each other such that assignments to a variable are performed before reads of the variable, including scheduling the assignment operations to the variable that are concurrent with each other such that a first assignment operation is scheduled before one or more other assignment operations, wherein the order of the one or more other assignment operations does not influence a final result of the variable for the logical tick; and
validating the program in accordance with the specified model of computation in response to said determining.
8. The computer system of claim 7 , wherein the operations further include:
compiling the program to produce output code that is deterministically executable.
9. The computer system of claim 7 ,
wherein said determining that the program has deterministic semantics is based on specification of sequencing information by the program specifying sequencing for at least a portion of the plurality of operations; and
wherein the specified model of computation is a sequential model of computation.
10. The method of claim 1 , wherein the one or more other assignment operations are relative assignment operations and the first assignment operation is an absolute assignment operation.
11. The method of claim 1 , wherein the one or more other assignment operations specify the same commutative and associative operation.
12. The computer system of claim 7 , wherein the one or more other assignment operations are relative assignment operations and the first assignment operation is an absolute assignment operation.
13. The computer system of claim 7 , wherein the one or more other assignment operations specify the same operation and wherein the operation is a commutative and associative operation.
14. A non-transitory computer-readable medium having computer instructions stored thereon that are capable of causing operations comprising:
receiving a program, wherein the program specifies a plurality of operations using a variable within a logical tick such that the variable has multiple values within the logical tick;
statically analyzing the program according to a specified model of computation that specifies program execution based on logical ticks, wherein said statically analyzing the program includes:
determining that the program has deterministic semantics, wherein the deterministic semantics 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;
wherein the deterministic semantics is based on, within a given logical tick:
a scheduling of operations that are sequential with respect to each other as specified by the program according to the specified sequence; and
a scheduling of operations that are concurrent with each other such that assignments to a variable are performed before reads of the variable, including scheduling the assignment operations to the variable that are concurrent with each other such that a first assignment operation is scheduled before one or more other assignment operations, wherein the order of the one or more other assignment operations does not influence a final result of the variable for the logical tick; and
validating the program in accordance with the specified model of computation in response to said determining.