From 29ec67340c03fb15dce465381737b96e12ef764b Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Sat, 28 Oct 2023 15:57:52 +0900 Subject: Draft skeleton --- glossary.tex | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 glossary.tex (limited to 'glossary.tex') 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}} -- cgit 1.4.1