-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
All: added new obsidian notes for autumn term 4th year
- Loading branch information
1 parent
6afaef8
commit 070683c
Showing
163 changed files
with
3,585 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
{ | ||
"userIgnoreFilters": [ | ||
"50001 - Algorithm Analysis and Design/", | ||
"50003 - Models of Computation/", | ||
"50005 - Networks and Communications/", | ||
"50006 - Compilers/", | ||
"50008 - Probability and Statistics/", | ||
"60001 - Advanced Computer Architecture/", | ||
"60007 - Theory and Practice of Concurrent Programming/", | ||
"60008 - Custom Computing/", | ||
"60009 - Distributed Algorithms/", | ||
"60017 - System Performance Engineering/", | ||
"60023 - Type Systems for Programming Languages/", | ||
"60029 - Data Processing Systems/", | ||
"common/", | ||
"tools/", | ||
"README", | ||
"LICENCE" | ||
] | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
{ | ||
"accentColor": "" | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
[] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
{ | ||
"file-explorer": true, | ||
"global-search": true, | ||
"switcher": true, | ||
"graph": true, | ||
"backlink": true, | ||
"canvas": true, | ||
"outgoing-link": true, | ||
"tag-pane": true, | ||
"properties": false, | ||
"page-preview": true, | ||
"daily-notes": true, | ||
"templates": true, | ||
"note-composer": true, | ||
"command-palette": true, | ||
"slash-command": false, | ||
"editor-status": true, | ||
"bookmarks": true, | ||
"markdown-importer": false, | ||
"zk-prefixer": false, | ||
"random-note": false, | ||
"outline": true, | ||
"word-count": true, | ||
"slides": false, | ||
"audio-recorder": false, | ||
"workspaces": false, | ||
"file-recovery": true, | ||
"publish": false, | ||
"sync": false | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
[ | ||
"file-explorer", | ||
"global-search", | ||
"switcher", | ||
"graph", | ||
"backlink", | ||
"canvas", | ||
"outgoing-link", | ||
"tag-pane", | ||
"page-preview", | ||
"daily-notes", | ||
"templates", | ||
"note-composer", | ||
"command-palette", | ||
"editor-status", | ||
"bookmarks", | ||
"outline", | ||
"word-count", | ||
"file-recovery" | ||
] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
{ | ||
"collapse-filter": true, | ||
"search": "", | ||
"showTags": false, | ||
"showAttachments": false, | ||
"hideUnresolved": false, | ||
"showOrphans": true, | ||
"collapse-color-groups": true, | ||
"colorGroups": [], | ||
"collapse-display": true, | ||
"showArrow": false, | ||
"textFadeMultiplier": 0, | ||
"nodeSizeMultiplier": 1, | ||
"lineSizeMultiplier": 1, | ||
"collapse-forces": true, | ||
"centerStrength": 0.518713248970312, | ||
"repelStrength": 10, | ||
"linkStrength": 1, | ||
"linkDistance": 250, | ||
"scale": 0.1846232622585825, | ||
"close": false | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
{} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,182 @@ | ||
{ | ||
"main": { | ||
"id": "c4b3f9b423457a3e", | ||
"type": "split", | ||
"children": [ | ||
{ | ||
"id": "b31f72987442726a", | ||
"type": "tabs", | ||
"children": [ | ||
{ | ||
"id": "ae21474f075e159a", | ||
"type": "leaf", | ||
"state": { | ||
"type": "markdown", | ||
"state": { | ||
"file": "README.md", | ||
"mode": "source", | ||
"source": false | ||
} | ||
} | ||
} | ||
] | ||
} | ||
], | ||
"direction": "vertical" | ||
}, | ||
"left": { | ||
"id": "349c566ccce2bac3", | ||
"type": "split", | ||
"children": [ | ||
{ | ||
"id": "fbadf7df1bb69fe8", | ||
"type": "tabs", | ||
"children": [ | ||
{ | ||
"id": "7b7b1ea9a95d8ea6", | ||
"type": "leaf", | ||
"state": { | ||
"type": "file-explorer", | ||
"state": { | ||
"sortOrder": "alphabetical" | ||
} | ||
} | ||
}, | ||
{ | ||
"id": "487ae844bcec21a3", | ||
"type": "leaf", | ||
"state": { | ||
"type": "search", | ||
"state": { | ||
"query": "", | ||
"matchingCase": false, | ||
"explainSearch": false, | ||
"collapseAll": false, | ||
"extraContext": false, | ||
"sortOrder": "alphabetical" | ||
} | ||
} | ||
}, | ||
{ | ||
"id": "5a1ef71029dce8b4", | ||
"type": "leaf", | ||
"state": { | ||
"type": "bookmarks", | ||
"state": {} | ||
} | ||
} | ||
] | ||
} | ||
], | ||
"direction": "horizontal", | ||
"width": 300 | ||
}, | ||
"right": { | ||
"id": "f80d2a15938ae6ce", | ||
"type": "split", | ||
"children": [ | ||
{ | ||
"id": "d07aecd7a14d3724", | ||
"type": "tabs", | ||
"children": [ | ||
{ | ||
"id": "0ee7da668cf93dcb", | ||
"type": "leaf", | ||
"state": { | ||
"type": "backlink", | ||
"state": { | ||
"file": "README.md", | ||
"collapseAll": false, | ||
"extraContext": false, | ||
"sortOrder": "alphabetical", | ||
"showSearch": false, | ||
"searchQuery": "", | ||
"backlinkCollapsed": false, | ||
"unlinkedCollapsed": true | ||
} | ||
} | ||
}, | ||
{ | ||
"id": "e3147701fdc6e933", | ||
"type": "leaf", | ||
"state": { | ||
"type": "outgoing-link", | ||
"state": { | ||
"file": "README.md", | ||
"linksCollapsed": false, | ||
"unlinkedCollapsed": true | ||
} | ||
} | ||
}, | ||
{ | ||
"id": "9c2c08320c062b9b", | ||
"type": "leaf", | ||
"state": { | ||
"type": "tag", | ||
"state": { | ||
"sortOrder": "frequency", | ||
"useHierarchy": true | ||
} | ||
} | ||
}, | ||
{ | ||
"id": "cdc0190c6adf150b", | ||
"type": "leaf", | ||
"state": { | ||
"type": "outline", | ||
"state": { | ||
"file": "README.md" | ||
} | ||
} | ||
} | ||
] | ||
} | ||
], | ||
"direction": "horizontal", | ||
"width": 300, | ||
"collapsed": true | ||
}, | ||
"left-ribbon": { | ||
"hiddenItems": { | ||
"switcher:Open quick switcher": false, | ||
"graph:Open graph view": false, | ||
"canvas:Create new canvas": false, | ||
"daily-notes:Open today's daily note": false, | ||
"templates:Insert template": false, | ||
"command-palette:Open command palette": false | ||
} | ||
}, | ||
"active": "ae21474f075e159a", | ||
"lastOpenFiles": [ | ||
"60029 - Data Processing Systems/advanced_topics/code/partition_comparison/build/_deps/googletest-src/docs/quickstart-bazel.md", | ||
"70020 - Program Analysis/Extraction Function.md", | ||
"70020 - Program Analysis/Power Set.md", | ||
"70020 - Program Analysis/Orthogonal Projections.md", | ||
"70020 - Program Analysis/Partial Order.md", | ||
"70020 - Program Analysis/Partial Function.md", | ||
"70020 - Program Analysis/Normed Vector Spaces.md", | ||
"70020 - Program Analysis/Must Analysis.md", | ||
"70020 - Program Analysis/MOP.md", | ||
"70020 - Program Analysis/Live Variable Analysis.md", | ||
"70020 - Program Analysis/Moore-Penrose Generalised Inverse.md", | ||
"70020 - Program Analysis/Monte Carlo Algorithms.md", | ||
"70020 - Program Analysis/Monotone Framework.md", | ||
"70020 - Program Analysis/MFP.md", | ||
"70020 - Program Analysis/May Analysis.md", | ||
"70020 - Program Analysis/LV Constraints.md", | ||
"70020 - Program Analysis/Linear Operator Semantics.md", | ||
"70020 - Program Analysis/Lattice Equations.md", | ||
"70020 - Program Analysis/Las Vegas Algorithm.md", | ||
"70020 - Program Analysis/Isolated Entries & Exits.md", | ||
"70020 - Program Analysis/Label Consistency.md", | ||
"70020 - Program Analysis/Isomorphism.md", | ||
"70020 - Program Analysis/Fixed Point.md", | ||
"70020 - Program Analysis/Inner Product.md", | ||
"70020 - Program Analysis/Fun Language for Program Analysis.md", | ||
"70020 - Program Analysis/Halting Problem.md", | ||
"70020 - Program Analysis/abstract interpretation.drawio.svg", | ||
"70020 - Program Analysis/abstract interpretation general construction.drawio.svg", | ||
"70020 - Program Analysis", | ||
"70025 - Software Engineering for Industry" | ||
] | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
## Definition | ||
Requires [[Abstract Domains]] and a specification of the analysis to produce $(\widehat{C}, \widehat{\rho})$ | ||
- $\widehat{C}$ is an [[Abstract Domains#Abstract Cache]] (*shape* of the label) | ||
- $\widehat{\rho}$ is the [[Abstract Domains#Abstract Environment]] that associates values with each variable (*shape* of the variables) | ||
We have the entails relation: | ||
$$\vDash \ : (\widehat{\mathbf{Cache}} \times \widehat{\mathbf{Env}} \times \mathbf{Exp}) \to \{true, false\} | ||
\qquad \qquad (\widehat{C}, \widehat{\rho}) \vDash e$$ Which means we have an acceptable [[Control Flow Analysis]]for expression $e$. | ||
- If a subexpression $t^\ell$ evaluates to a closure, then the closure must be predicted by $\widehat{C}(\ell)$ | ||
This analysis is not [[Context Sensitive]] and in [[Control Flow Analysis]] terminology is [[Monovariant]]. | ||
## Rules | ||
### Constants | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_s c^\ell \quad \text{always}$$ | ||
Since we care about closures only, constants are irrelevant. | ||
### Terms | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_s x^\ell \Longleftrightarrow \widehat{\rho}(x) \subseteq \widehat{C}(\ell)$$ | ||
The variable contains the same value as is predicted by the [[Abstract Domains#Abstract Cache|cache]]. | ||
### if-else | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_s \left[\mathbf{if} \ t_0^{\ell_0} \ \mathbf{then} \ t_1^{\ell_1} \ \mathbf{else} \ t_2^{\ell_2}\right]^\ell \ \Longleftrightarrow \begin{split} | ||
& (\widehat{C}, \widehat{\rho}) \vDash_s t_0^{\ell_0} \land (\widehat{C}, \widehat{\rho}) \vDash_s t_1^{\ell_1} \land (\widehat{C}, \widehat{\rho}) \vDash_s t_2^{\ell_2} \\ | ||
\land & \ \widehat{C}(\ell_1) \subseteq \widehat{C}(\ell) \\ | ||
\land & \ \widehat{C}(\ell_2) \subseteq \widehat{C}(\ell) | ||
\end{split}$$ | ||
The [[Abstract Domains#Abstract Cache|cache]] must contain the terms for both branches (& whence what this label could be). | ||
### Let | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_s \left[ \mathbf{let} \ x = t_1^{\ell_1} \ \mathbf{in} \ t_2^{\ell_2} \right]^\ell \Longleftrightarrow \begin{split} | ||
& (\widehat{C}, \widehat{\rho}) \vDash_s t_1^{\ell_1} \land (\widehat{C}, \widehat{\rho}) \vDash_s t_2^{\ell_2}\\ | ||
\land & \ \widehat{C}(\ell_1) \subseteq \widehat{\rho}(x) \\ | ||
\land & \ \widehat{C}(\ell_2) \subseteq \widehat{C}(\ell) \\ | ||
\end{split}$$ | ||
Like with [[0-CFA Analysis#if-else|if-else]] we need the [[Abstract Domains#Abstract Cache|cache]] to have the *shape* of $\ell$, but now we need to ensure that $\widehat{\rho}$ also has the shape of $x$. | ||
### Operator | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_x \left[ t_1^{\ell_1} \ op \ t_2^{\ell_2} \right]^\ell \Longleftrightarrow (\widehat{C}, \widehat{\rho}) \vDash_s t_1^{\ell_1} \land (\widehat{C}, \widehat{\rho}) \vDash_s t_2^{\ell_2}$$ | ||
$\widehat{C}$ must have the shape of both sides, as $op$ is assumed to be $+,-,\times, \div$ we assume its shape is not a closure. | ||
### Closure | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_x \left[\mathbf{fn} \ x \Rightarrow e_0 \right]^\ell \Longleftrightarrow \{\mathbf{fn} \ x \Rightarrow e_0\} \subseteq \widehat{C}(\ell) \land (\widehat{C}, \widehat{\rho}) \vDash_s e_0$$ | ||
We can include $\ell$ in $\widehat{C}$ because we assume [[Label Consistency]]. | ||
### Application | ||
$$(\widehat{C}, \widehat{\rho}) \vDash_x \left[ t_1^{\ell_1} \ t_2^{\ell_2}\right]^\ell \Longleftrightarrow \begin{split} | ||
& (\widehat{C}, \widehat{\rho}) \vDash_s t_1^{\ell_1} \land (\widehat{C}, \widehat{\rho}) \vDash_s t_2^{\ell_2} \\ | ||
\land & \left( \forall (\mathbf{fn} \ x \Rightarrow t_0^{\ell_0}) \in \widehat{C}(\ell_1) : \widehat{C}(\ell_2) \subseteq \widehat{\rho}(x) \land \widehat{C}(\ell_0) \subseteq \widehat{C}(\ell) \right) \\ | ||
\end{split}$$ | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
## Definition | ||
An *Abelian Group* is a commutative [[Group]]. An *Additive Group* is a [[Group]] with a $\bullet$ that is analogous/should be thought of as additive in some way. | ||
- (*Abelian Group*) For a group $G$ $\forall a, b \in G : a \bullet b = b \bullet a$ | ||
- (*Additive Group*) We can write $\bullet$ as $+$ instead | ||
|
||
## Examples | ||
### Integer Sets | ||
$$\text{For some } X \ \text{ we can have }(\mathcal{P}(X), \emptyset, \cup)$$ | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
## Definition | ||
- Can be compared with the [[Fun Language for Program Analysis#Concrete Domain]]. | ||
### Abstract Environment | ||
$$\widehat{\rho} \in \widehat{\mathbf{Env}} = \mathbf{Var} \to \widehat{\mathbf{Val}}$$ | ||
- Maps variables to an abstract value | ||
### Abstract Cache | ||
$$\widehat{C} \in \widehat{\mathbf{Cache}} = \mathbf{Lab} \to \widehat{\mathbf{Val}}$$ | ||
### Abstract Value | ||
$$\widehat{v} \in \widehat{\mathbf{Val}} = \mathcal{P}(\mathbf{Term})$$ | ||
- A set of terms of the form $\mathbf{fn} \ x \Rightarrow e_0$ |
Oops, something went wrong.