-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathengineering.txt
85 lines (63 loc) · 3.79 KB
/
engineering.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
engineering.txt 0.0.2 UTF-8 2023-11-08
----|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
MISER THEORETICAL CONCEPTION
============================
BACKGROUND HISTORY OF THE MISER PROJECT
---------------------------------------
<https://github.com/orcmid/miser/blob/master/engineering.txt>
[SYNOPSIS: TBD]
[CONTENT: TBD]
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Copyright 2018-2019, 2023 Dennis E. Hamilton
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
TODO
* <https://www.engineering.columbia.edu/news/new-tool-automates-formal-verification-systems-software>
a COQ-based system that may provide practical verification of C Language
programs. This may be important/useful in verifying oMiser at some point.
<https://www.usenix.org/conference/osdi23/presentation/li-xupeng> is the
Usenix conference presentation.
* Transform the TODOs into sections of History, Current Challenges, and
references/bibliography.
* Find other TODOs of this nature and transpose them to this file.
* Engineering is about dependability and reliability of implementations,
along with achievement of confirmable experiences, replication/
reproducibility of results, and a reliable development process.
* Having a low-end-of-the-pool on-ramp for developers is an important
aspect. Reflect this.
* Introduce a section on use of a list-structured storage system.
o employ reference counting for enduring constructions
o employ Cheney copying and the Henry Baker techniques for seemingly
ephemeral constructions
o consider what is facilitated by immutability with respect to having
coalescing of identical obs-in-storage and also accelerated applicative
interpretations of obs.
* Discuss the ob.c equality proposition and how to accelerate it.
o when two pointers to obs are the same, we know the obs are identical.
o if individuals have different locations, we know they are different.
o when two pointers to obs are different, we know we have to compare the
components.
o if we find that the corresponding components are equal, we can substitute
the older one for the younger in wherever the younger link is anchored.
o if we have hashes, we can know that two obs are different if there
hashes are different. But if they are the same, we have to look
further because there may simply be a hash collision.
o the use of hashes for acceleration of comparisons in LISP was mentioned
to me by Paul McJones. Find a link to that.
o When obs have accelerated applicative interpretations, and they are found
to be equal, we need to determine what to do when the younger has
an/the accelerator.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
0.0.2 2023-11-08T20:08Z Add information on SPOQ
0.0.1 2019-10-13-13:01 Add notes on storage implementation, comparison
shortening and applicative interpretation accelerators.
0.0.0 2018-04-17-10:29 Create placeholder, with starter TODOs.
*** end of engineering.txt ***