-
Notifications
You must be signed in to change notification settings - Fork 0
/
londongophers-aug18.slide
200 lines (120 loc) · 4.4 KB
/
londongophers-aug18.slide
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
Building a simple concurrency teaching language with Go
15 Aug 2018
Nicholas Ng
Imperial College London
nickng@nickng.io
@nicholascwng
* About me
Postdoc @ Imperial College
- Formal concurrency models
- Programming languages: types and static analysis/verification
* Concurrency @ IC
- Model, analyse, program concurrent systems
- Concurrency issues (deadlock etc.)
Disclaimer - course is not directly related to talk
* Formal models of concurrency
The actor model
- Proposed by Carl Hewitt; foundation of Erlang/Elixir
- Concurrent *actors* react to incoming message
Process calculi
- Family of related models with many variants
- Most well known: Hoare's CSP, Milner's CCS and π-calculus
- Concurrent *processes* synchronise by communication (message passing)
Alternatives
- e.g. Petri nets
* Formal concurrency models vs. Concurrent programming
Formal concurrency models
- Abstract
- Pen and paper
Concurrent programming
- Concrete language
- Executable
🤔 Executable formal model?
* asyncpi: A teaching language based on "asynchronous π-calculus"
.link http://go.nickng.io/asyncpi
.image pi.png
.caption The asynchronous π-calculus (Honda, Tokoro 1991; Boudol 1992)
Objectives
- Write down machine-readable formal processes
- Explore how processes evolve (through communication)
- Generate example concurrent code in Go
* This talk
- asyncpi is just an example
- Implement a small (executable) domain-specific language
- Tools and packages that I find useful
* The asyncpi language
.code grammar.txt
A *grammar* specifies the syntax of the language, e.g.
.code syntax_example.pi
Objective: make this input machine-readable
* Parsing
Read stream of symbols of given grammar into abstract syntax tree
.play parse_syntax.go /^func main/,/^}/
Implement Parse by fmt.Scanf?
* golang.org/x/tools/cmd/goyacc
*yacc* (Yet Another Compiler-Compiler) is a _parser_generator_
- Input: grammar, output: parser
- Your code convert valid parsed input to your representation (e.g. AST)
- Not just for "languages", config files, structured data files, etc.
- *goyacc* is a Go port of the tool
.link https://github.com/nickng/asyncpi/blob/master/asyncpi.y
.code goyacc.txt
More about parsing with Go
.link https://blog.golang.org/generate Generating code (The Go blog)
.link https://blog.gopheracademy.com/advent-2014/parsers-lexers/ Handwritten Parsers & Lexers in Go (Gopher Academy)
* go generate
- Part of the go tool chain
- Runs an _arbitrary_ command (does not have to generate code!)
Instead of
.code goyacc.sh
Put this in a .go file:
.code goyacc.go
* Objectives
- Write down machine-readable formal process ✔️
- Explore how processes evolve (through communication)
- Generate example concurrent code in Go
* Process reduction
- What we parsed: snapshot of concurrent system
- _Communicate_ if shared channel exists
- Evolve system by _reducing_ both sub-processes
.image reduction.svg
We can write code to *reduce* in Go..
* Process reduction
- What we parsed: snapshot of concurrent system
- _Communicate_ if shared channel exists
- Evolve system by _reducing_ both sub-processes
.play -edit sendrecv_reduce.go /^func main/,/^}/
* Play with processes in Go
.play sendrecv_reduce2.go /^func main/,/^}/
* Objectives
- Write down machine-readable formal process ✔️
- Explore how process evolve (through communication) ✔️
- Generate example concurrent code in Go
* Generate Go code from asyncpi
.play sendrecv_codegen.go /^func main/,/^}/
- Not very sophisticated (uses text/template package)
- Not idiomatic Go
* go/format package
Every Go programmer should know "gofmt"
You can also use go/format to format Go code (snippets)
.play -edit sendrecv_gofmt.go /^func main/,/^}/
* golang.org/x/tools/imports package
You can also use imports to fix imports
.play -edit sendrecv_goimports.go /^func main/,/^}/
* Another use of generating Go code
- Both `sendrecv` and `chainReaction` processes reduce to 0
- What if it doesn't?
.play sendrecvrecv.go /^func main/,/^}/
* Objectives
- Write down machine-readable formal process ✔️
- Explore how processes evolve (through communication) ✔️
- Generate example concurrent code in Go ✔️
* Summary
- A concurrency teaching language called asyncpi
- Parse asyncpi process into Go program
- Programmatically use the process
- Generate and format Go code and gofmt way
* More?
- REPL
- Channel types and type inference (Hindley-Milner)
- Formal model to Go code _and_back_