diff options
author | Nguyễn Gia Phong <cnx@loang.net> | 2023-10-28 15:57:52 +0900 |
---|---|---|
committer | Nguyễn Gia Phong <cnx@loang.net> | 2023-10-28 20:02:06 +0900 |
commit | 29ec67340c03fb15dce465381737b96e12ef764b (patch) | |
tree | 31a07da1af8c4fa05f64e2fb52a3bfcdbdab3c5c /glossary.tex | |
download | thesis-29ec67340c03fb15dce465381737b96e12ef764b.tar.gz |
Draft skeleton
Diffstat (limited to 'glossary.tex')
-rw-r--r-- | glossary.tex | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/glossary.tex b/glossary.tex new file mode 100644 index 0000000..8f43f5f --- /dev/null +++ b/glossary.tex @@ -0,0 +1,32 @@ +\makenoidxglossaries +\newglossaryentry{difftest}{name={differential test}, + description={Is an input and a collection of outputs of two or more programs + of the same purpose, such that each output is pairwise different}} +\newglossaryentry{state}{name=state, + description={Or \emph{symbolic process}, includes a register file, + a stack frame, an address space for heap and global variables, + a program counter and path conditions. Stack, heap and global variables + here are all symbolic expressions. For our algorithm, the state + additionally contain the identifier of its program revision}} +\newglossaryentry{pstates}{name={parallel states}, + description={Two states are parallel if and only if their program counter + points to the same instruction\footnote{They do not necessarily + share the same program counter however.} and the conjunction + of their path conditions is satisfiable}} +\newglossaryentry{searcher}{name=searcher, + description={Is what keeps track of states to be executed, + along with the information for scheduling them to optimize resources + on the progress of reaching the goal. In this work, the searcher + includes a set of states and execution frontier tracking}} +\newglossaryentry{execfront}{name={execution frontier}, + description={An instruction $i$ is said to be an execution frontier + of the other $j$ if and only if there exists an execution path + in which the first occurrence of $i$ is before that of $j$. + In more relaxed terminologies, a state $s$ is said to be a frontier + of the other state $z$ if $s$'s program counter is a frontier of $z$'s}} +\newglossaryentry{lexecfront}{name={local execution frontier}, + description={Between a program's states, those not having a frontier + are called the local execution frontiers}} +\newglossaryentry{gexecfront}{name={global execution frontier}, + description={Between the states of multiple program's revisions, + those not having an frontier are called the global execution frontiers}} |