Detection of Harmful Schizophrenic Statements in Esterel
In imperative synchronous languages, a statement is called schizophrenic if it is executed more than once in a single clock. When a schizophrenic statement is translated into a circuit, the circuit can behave abnormally because of the multiple executions. To solve the problems caused by schizophrenic statements, compilers duplicate the statements to avoid multiple executions. Esterel is an imperative synchronous language. Schizophrenic statements in Esterel are considered to occur due to the instantaneous reentrance of local signal declarations or parallel statements. However, if the corresponding circuit of a schizophrenic statement behaves normally, it is harmless and thus curing is not necessary. In this paper, we identify the conditions under which a schizophrenic statement of the Esterel program must be cured during circuit translation. We also propose an algorithm to detect schizophrenic statements that have to be cured on the control flow graphs (CFGs) of source codes. Our algorithm detects all schizophrenic statements that have to be cured and results in fewer false alarms on the benchmark programs used in the previous work. It is simple and based on the CFG of a program, implying that it can be merged into existing compilers easily.
synchronous languages languages algorithms verification static analysis