-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathreferences.bib
2840 lines (2627 loc) · 228 KB
/
references.bib
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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
@misc{linux_kernel_newbies_editors_linux_2020,
type = {Wiki},
title = {Linux {Version} 5.6 {Changelog}},
url = {https://kernelnewbies.org/Linux_5.6},
urldate = {2022-04-20},
journal = {Linux Kernel Newbies},
author = {Linux Kernel Newbies Editors},
month = mar,
year = {2020},
}
@misc{linux_kernel_newbies_editors_linux_2008,
type = {Wiki},
title = {Linux {Version} 2.6.24 {Changelog}},
url = {https://kernelnewbies.org/Linux_2_6_24},
urldate = {2022-04-20},
journal = {Linux Kernel Newbies},
author = {Linux Kernel Newbies Editors},
month = jan,
year = {2008},
}
@misc{linux_kernel_newbies_editors_linux_2007,
type = {Wiki},
title = {Linux {Version} 2.6.23 {Changelog}},
url = {https://kernelnewbies.org/Linux_2_6_23},
urldate = {2022-04-20},
journal = {Linux Kernel Newbies},
author = {Linux Kernel Newbies Editors},
month = oct,
year = {2007},
}
@misc{linux_kernel_newbies_editors_linux_2006,
type = {Wiki},
title = {Linux {Version} 2.6.19 {Changelog}},
url = {https://kernelnewbies.org/Linux_2_6_19},
urldate = {2022-04-20},
journal = {Linux Kernel Newbies},
author = {Linux Kernel Newbies Editors},
month = nov,
year = {2006},
}
@inproceedings{accetta_mach_1986,
title = {Mach: {A} {New} {Kernel} {Foundation} for {UNIX} {Development}},
booktitle = {Proceedings of the {USENIX} {Summer} {Conference}, {Altanta}, {GA}, {USA}, {June} 1986},
publisher = {USENIX Association},
author = {Accetta, Michael J. and Baron, Robert V. and Bolosky, William J. and Golub, David B. and Rashid, Richard F. and Tevanian, Avadis and Young, Michael},
year = {1986},
pages = {93--113},
}
@article{accetta_mach_nodate,
title = {Mach: {A} {New} {Kernel} {Foundation} {For} {UNIX} {Development}},
abstract = {Mach is a multiprocessor operating system kernel and environment under development at Carnegie Mellon University. Mach provides a new foundation for UNIX development that spans networks of uniprocessors and multiprocessors. This paper describes Mach and the motivations that led to its design. Also described are some of the details of its implementation and current status.},
language = {en},
author = {Accetta, Mike and Baron, Robert and Bolosky, William and Golub, David and Rashid, Richard and Tevanian, Avadis and Young, Michael},
pages = {16},
}
@misc{the_openbsd_foundation_openssh_2022,
title = {{OpenSSH} 8.9 {Release} {Notes}},
url = {https://www.openssh.com/txt/release-8.9},
urldate = {2022-05-12},
journal = {OpenSSH},
author = {The OpenBSD Foundation},
month = feb,
year = {2022},
}
@inproceedings{staniford_how_2002,
title = {How to own the internet in your spare time},
url = {https://www.usenix.org/legacy/event/sec02/full_papers/staniford/staniford_html/},
urldate = {2022-05-11},
booktitle = {11th {USENIX} {Security} {Symposium} ({USENIX} {Security} 02)},
author = {Staniford, Stuart and Paxson, Vern and Weaver, Nicholas},
year = {2002},
}
@misc{the_mitre_corporation_deserialization_2006,
title = {Deserialization of {Untrusted} {Data} (4.7)},
url = {https://cwe.mitre.org/data/definitions/502.html},
abstract = {The software constructs a string for a command to executed by a separate component in another control sphere, but it does not properly delimit the intended arguments, options, or switches within that command string.},
urldate = {2022-05-09},
journal = {Common Weakness Enumeration},
author = {The MITRE Corporation},
month = jul,
year = {2006},
}
@misc{the_mitre_corporation_improper_2006,
title = {Improper {Neutralization} of {Argument} {Delimiters} in a {Command} ('{Argument} {Injection}') (4.7)},
url = {https://cwe.mitre.org/data/definitions/88.html},
abstract = {The software constructs a string for a command to executed by a separate component in another control sphere, but it does not properly delimit the intended arguments, options, or switches within that command string.},
urldate = {2022-05-09},
journal = {Common Weakness Enumeration},
author = {The MITRE Corporation},
month = jul,
year = {2006},
}
@misc{madhavapeddy_privsepc_2003,
title = {privsep.c},
url = {https://cvsweb.openbsd.org/cgi-bin/cvsweb/src/usr.sbin/syslogd/privsep.c?rev=1.1&content-type=text/x-cvsweb-markup},
abstract = {Privilege separated syslog daemon. The child listening to log requests drops
to user \_syslogd and chroots itself, while the privileged parent grants it
access to open logfiles and other calls it needs.},
urldate = {2022-05-09},
journal = {OpenBSD CVS Repository},
author = {Madhavapeddy, Anil},
month = jul,
year = {2003},
}
@misc{the_openbsd_foundation_pledge2_2022,
title = {pledge(2)},
url = {https://man.openbsd.org/pledge.2},
urldate = {2022-05-03},
journal = {OpenBSD manual pages},
author = {The OpenBSD Foundation},
month = feb,
year = {2022},
}
@misc{loscocco_security-enhanced_2000,
type = {Mailing {List}},
title = {Security-enhanced {Linux} available at {NSA} site},
url = {https://lore.kernel.org/all/[email protected]/},
urldate = {2022-05-03},
journal = {lore.kernel.org},
author = {Loscocco, Pete},
month = dec,
year = {2000},
}
@misc{the_systemd_authors_systemdslice_2022,
title = {systemd.slice},
url = {https://www.freedesktop.org/software/systemd/man/systemd.slice.html},
urldate = {2022-05-03},
journal = {systemd Manual Pages},
author = {The Systemd Authors},
year = {2022},
}
@article{merkel_docker_2014,
title = {Docker: lightweight {Linux} containers for consistent development and deployment},
volume = {2014},
issn = {1075-3583},
shorttitle = {Docker},
abstract = {Docker promises the ability to package applications and their dependencies into lightweight containers that move easily between different distros, start up quickly and are isolated from each other.},
number = {239},
journal = {Linux Journal},
author = {Merkel, Dirk},
month = mar,
year = {2014},
pages = {2:2},
}
@misc{free_software_foundation_ipc_namespaces7_2021,
title = {ipc\_namespaces(7)},
url = {https://man7.org/linux/man-pages/man7/ipc_namespaces.7.html},
urldate = {2022-04-21},
journal = {Linux manual page},
author = {Free Software Foundation},
year = {2021},
}
@misc{free_software_foundation_time_namespaces7_2021,
title = {time\_namespaces(7)},
url = {https://man7.org/linux/man-pages/man7/time_namespaces.7.html},
urldate = {2022-04-21},
journal = {Linux manual page},
author = {Free Software Foundation},
year = {2021},
}
@misc{biederman_net_2007,
title = {[{NET}]: {Basic} network namespace infrastructure.},
url = {https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=5f256becd868bf63b70da8f2769033d6734670e9},
abstract = {This is the basic infrastructure needed to support network
namespaces. This infrastructure is:
- Registration functions to support initializing per network
namespace data when a network namespaces is created or destroyed.
- struct net. The network namespace data structure.
This structure will grow as variables are made per network
namespace but this is the minimal starting point.
- Functions to grab a reference to the network namespace.
I provide both get/put functions that keep a network namespace
from being freed. And hold/release functions serve as weak references
and will warn if their count is not zero when the data structure
is freed. Useful for dealing with more complicated data structures
like the ipv4 route cache.
- A list of all of the network namespaces so we can iterate over them.
- A slab for the network namespace data structure allowing leaks
to be spotted.},
urldate = {2022-04-20},
journal = {Linux kernel source tree},
author = {Biederman, Eric W.},
month = oct,
year = {2007},
}
@misc{vagin_ns_2020,
title = {ns: {Introduce} {Time} {Namespace}},
url = {https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=769071ac9f20b6a447410c7eaa55d1a5233ef40c},
abstract = {Time Namespace isolates clock values.},
urldate = {2022-04-20},
journal = {Linux kernel source tree},
author = {Vagin, Andrei},
month = jan,
year = {2020},
}
@misc{bhattiprolu_patch_2006,
title = {[{PATCH}] {Define} struct pspace},
url = {https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=3fbc96486459324e182717b03c50c90c880be6ec},
abstract = {Define a per-container pid space object. And create one instance of this object, init\_pspace, to define the entire pid space. Subsequent patches will provide/use interfaces to create/destroy pid spaces.},
urldate = {2022-04-20},
journal = {Linux kernel source tree},
author = {Bhattiprolu, Sukadev},
month = oct,
year = {2006},
}
@misc{le_goater_user_2007,
title = {user namespace: add the framework},
url = {https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=acce292c82d4d82d35553b928df2b0597c3a9c78},
abstract = {Basically, it will allow a process to unshare its user\_struct table, resetting at the same time its own user\_struct and all the associated accounting.},
urldate = {2022-04-20},
journal = {Linux kernel source tree},
author = {Le Goater, Cedric},
month = jul,
year = {2007},
}
@misc{hallyn_patch_2006,
title = {[{PATCH}] namespaces: utsname: implement utsname namespaces},
url = {https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=4865ecf1315b450ab3317a745a6678c04d311e40},
abstract = {This patch defines the uts namespace and some manipulators. Adds the uts namespace to task\_struct, and initializes a system-wide init namespace.},
urldate = {2022-04-20},
journal = {Linux kernel source tree},
author = {Hallyn, Serge E.},
month = oct,
year = {2006},
}
@misc{korotaev_patch_2006,
title = {[{PATCH}] {IPC} namespace core},
url = {https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=25b21cb2f6d69b0475b134e0a3e8e269137270fa},
abstract = {This patch set allows to unshare IPCs and have a private set of IPC objects (sem, shm, msg) inside namespace. Basically, it is another building block of containers functionality.},
urldate = {2022-04-20},
journal = {Linux kernel source tree},
author = {Korotaev, Kirill},
month = oct,
year = {2006},
}
@misc{torvalds_linux_2002,
title = {Linux {Kernel} {Version} 2.5.2 {Changelog}},
url = {https://mirrors.edge.kernel.org/pub/linux/kernel/v2.5/ChangeLog-2.5.2},
urldate = {2022-04-20},
journal = {kernel.org},
author = {Torvalds, Linus},
month = jan,
year = {2002},
}
@misc{viro_patchcft_2001,
type = {Mailing {List}},
title = {[{PATCH}][{CFT}] per-process namespaces for {Linux}},
url = {https://lore.kernel.org/all/[email protected]/},
urldate = {2022-04-16},
journal = {lore.kernel.org},
author = {Viro, Alexander},
month = feb,
year = {2001},
}
@misc{viro_rfc_2005,
type = {Mailing {List}},
title = {[{RFC}] shared subtrees},
url = {https://lore.kernel.org/all/[email protected]/},
urldate = {2022-04-16},
journal = {lore.kernel.org},
author = {Viro, Alexander},
month = jan,
year = {2005},
}
@misc{pai_shared_2005,
title = {Shared {Subtrees}},
url = {https://www.kernel.org/doc/Documentation/filesystems/sharedsubtree.txt},
urldate = {2022-04-15},
author = {Pai, Ram and Viro, Alexander},
month = nov,
year = {2005},
note = {Added in commit 9cfcceea8f7e8f5554e9c8130e568bcfa98a3a64},
}
@misc{viro_patch_2001,
type = {Mailing {List}},
title = {[{PATCH}] lazy umount (1/4)},
url = {https://lore.kernel.org/all/[email protected]/},
urldate = {2022-04-16},
journal = {lore.kernel.org},
author = {Viro, Alexander},
month = sep,
year = {2001},
}
@misc{free_software_foundation_mount_namespaces7_2021,
title = {mount\_namespaces(7)},
url = {https://man7.org/linux/man-pages/man7/mount_namespaces.7.html},
urldate = {2022-04-15},
journal = {Linux manual page},
author = {Free Software Foundation},
year = {2021},
}
@misc{biederman_re_2007,
type = {Mailing {List}},
title = {Re: netns : close all sockets at unshare ?},
url = {https://lore.kernel.org/all/[email protected]/},
urldate = {2022-04-11},
journal = {lore.kernel.org},
author = {Biederman, Eric W.},
month = oct,
year = {2007},
}
@misc{torvalds_linux_2016,
type = {Mailing {List}},
title = {Linux 4.6-rc1},
url = {https://lore.kernel.org/all/CA+55aFzBncC+F8TEb5KU1QVwA=PCA89mDp1VLNq008oZq8vpJQ@mail.gmail.com/},
urldate = {2022-04-10},
journal = {lore.kernel.org},
author = {Torvalds, Linus},
month = mar,
year = {2016},
}
@misc{heo_git_2016,
type = {Mailing {List}},
title = {[{GIT} {PULL}] cgroup namespace support for v4.6-rc1},
url = {https://lore.kernel.org/all/[email protected]/#r},
abstract = {These are changes to implement namespace support for cgroup which has
been pending for quite some time now. It is very straight-forward and
only affects what part of cgroup hierarchies are visible. After
unsharing, mounting a cgroup fs will be scoped to the cgroups the task
belonged to at the time of unsharing and the cgroup paths exposed to
userland would be adjusted accordingly.},
urldate = {2022-04-10},
journal = {lore.kernel.org},
author = {Heo, Tejun},
month = mar,
year = {2016},
}
@inproceedings{madhavapeddy_jitsu_2015,
title = {Jitsu: \{{Just}-{In}-{Time}\} {Summoning} of {Unikernels}},
isbn = {978-1-931971-21-8},
shorttitle = {Jitsu},
url = {https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/madhavapeddy},
language = {en},
urldate = {2022-03-16},
author = {Madhavapeddy, Anil and Leonard, Thomas and Skjegstad, Magnus and Gazagnaire, Thomas and Sheets, David and Scott, Dave and Mortier, Richard and Chaudhry, Amir and Singh, Balraj and Ludlam, Jon and Crowcroft, Jon and Leslie, Ian},
year = {2015},
pages = {559--573},
}
@misc{gailly_gzip_2020,
title = {Gzip},
url = {https://www.gnu.org/software/gzip/},
urldate = {2022-03-14},
journal = {Gzip - GNU Project - Free Software Foundation},
author = {Gailly, Jean-loup},
month = aug,
year = {2020},
}
@misc{tea_hillion_nodate,
title = {Hillion {Gitea}},
url = {https://gitea.hillion.co.uk/},
abstract = {Gitea (Git with a cup of tea) is a painless self-hosted Git service written in Go},
language = {en-US},
urldate = {2022-03-13},
journal = {Hillion Gitea},
author = {tea, Gitea-Git with a cup of},
}
@inproceedings{padon_ivy_2016,
address = {New York, NY, USA},
series = {{PLDI} '16},
title = {Ivy: safety verification by interactive generalization},
isbn = {978-1-4503-4261-2},
shorttitle = {Ivy},
url = {https://doi.org/10.1145/2908080.2908118},
doi = {10.1145/2908080.2908118},
abstract = {Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system --- Ivy --- for interactively verifying safety of infinite-state systems. Ivy's key principle is that whenever verification fails, Ivy graphically displays a concrete counterexample to induction. The user then interactively guides generalization from this counterexample. This process continues until an inductive invariant is found. Ivy searches for universally quantified invariants, and uses a restricted modeling language. This ensures that all verification conditions can be checked algorithmically. All user interactions are performed using graphical models, easing the user's task. We describe our initial experience with verifying several distributed protocols.},
urldate = {2022-03-10},
booktitle = {Proceedings of the 37th {ACM} {SIGPLAN} {Conference} on {Programming} {Language} {Design} and {Implementation}},
publisher = {Association for Computing Machinery},
author = {Padon, Oded and McMillan, Kenneth L. and Panda, Aurojit and Sagiv, Mooly and Shoham, Sharon},
month = jun,
year = {2016},
keywords = {counterexamples to induction, distributed systems, invariant inference, safety verification},
pages = {614--630},
}
@inproceedings{nelson_scaling_2019,
address = {New York, NY, USA},
series = {{SOSP} '19},
title = {Scaling symbolic evaluation for automated verification of systems code with {Serval}},
isbn = {978-1-4503-6873-5},
url = {https://doi.org/10.1145/3341301.3359641},
doi = {10.1145/3341301.3359641},
abstract = {This paper presents Serval, a framework for developing automated verifiers for systems software. Serval provides an extensible infrastructure for creating verifiers by lifting interpreters under symbolic evaluation, and a systematic approach to identifying and repairing verification performance bottlenecks using symbolic profiling and optimizations. Using Serval, we build automated verifiers for the RISC-V, x86--32, LLVM, and BPF instruction sets. We report our experience of retrofitting CertiKOS and Komodo, two systems previously verified using Coq and Dafny, respectively, for automated verification using Serval, and discuss trade-offs of different verification methodologies. In addition, we apply Serval to the Keystone security monitor and the BPF compilers in the Linux kernel, and uncover 18 new bugs through verification, all confirmed and fixed by developers.},
urldate = {2022-03-07},
booktitle = {Proceedings of the 27th {ACM} {Symposium} on {Operating} {Systems} {Principles}},
publisher = {Association for Computing Machinery},
author = {Nelson, Luke and Bornholt, James and Gu, Ronghui and Baumann, Andrew and Torlak, Emina and Wang, Xi},
month = oct,
year = {2019},
pages = {225--242},
}
@inproceedings{ma_i4_2019,
address = {New York, NY, USA},
series = {{SOSP} '19},
title = {I4: incremental inference of inductive invariants for verification of distributed protocols},
isbn = {978-1-4503-6873-5},
shorttitle = {I4},
url = {https://doi.org/10.1145/3341301.3359651},
doi = {10.1145/3341301.3359651},
abstract = {Designing and implementing distributed systems correctly is a very challenging task. Recently, formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computer-checked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually---and painstakingly---by the developer. In this paper, we present a new approach, Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of a finite instance of the protocol can be used to infer a general inductive invariant for the infinite distributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC and Transaction Chains with little to no human effort.},
urldate = {2022-03-07},
booktitle = {Proceedings of the 27th {ACM} {Symposium} on {Operating} {Systems} {Principles}},
publisher = {Association for Computing Machinery},
author = {Ma, Haojun and Goel, Aman and Jeannin, Jean-Baptiste and Kapritsos, Manos and Kasikci, Baris and Sakallah, Karem A.},
month = oct,
year = {2019},
pages = {370--384},
}
@inproceedings{hawblitzel_ironfleet_2015,
address = {New York, NY, USA},
series = {{SOSP} '15},
title = {{IronFleet}: proving practical distributed systems correct},
isbn = {978-1-4503-3834-9},
shorttitle = {{IronFleet}},
url = {https://doi.org/10.1145/2815400.2815428},
doi = {10.1145/2815400.2815428},
abstract = {Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs a priori, but verification has historically been difficult to apply at full-program scale, much less distributed-system scale. We describe a methodology for building practical and provably correct distributed systems based on a unique blend of TLA-style state-machine refinement and Hoare-logic verification. We demonstrate the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification, as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct."},
urldate = {2022-03-07},
booktitle = {Proceedings of the 25th {Symposium} on {Operating} {Systems} {Principles}},
publisher = {Association for Computing Machinery},
author = {Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jacob R. and Parno, Bryan and Roberts, Michael L. and Setty, Srinath and Zill, Brian},
month = oct,
year = {2015},
pages = {1--17},
}
@inproceedings{song_practical_2000,
title = {Practical techniques for searches on encrypted data},
doi = {10.1109/SECPRI.2000.848445},
abstract = {It is desirable to store data on data storage servers such as mail servers and file servers in encrypted form to reduce security and privacy risks. But this usually implies that one has to sacrifice functionality for security. For example, if a client wishes to retrieve only documents containing certain words, it was not previously known how to let the data storage server perform the search and answer the query, without loss of data confidentiality. We describe our cryptographic schemes for the problem of searching on encrypted data and provide proofs of security for the resulting crypto systems. Our techniques have a number of crucial advantages. They are provably secure: they provide provable secrecy for encryption, in the sense that the untrusted server cannot learn anything about the plaintext when only given the ciphertext; they provide query isolation for searches, meaning that the untrusted server cannot learn anything more about the plaintext than the search result; they provide controlled searching, so that the untrusted server cannot search for an arbitrary word without the user's authorization; they also support hidden queries, so that the user may ask the untrusted server to search for a secret word without revealing the word to the server. The algorithms presented are simple, fast (for a document of length n, the encryption and search algorithms only need O(n) stream cipher and block cipher operations), and introduce almost no space and communication overhead, and hence are practical to use today.},
booktitle = {Proceeding 2000 {IEEE} {Symposium} on {Security} and {Privacy}. {S} {P} 2000},
author = {Song, Dawn Xiaoding and Wagner, D. and Perrig, A.},
month = may,
year = {2000},
note = {ISSN: 1081-6011},
keywords = {Authorization, Contracts, Cryptography, Data privacy, Data security, Electronic mail, File servers, Memory, Postal services, US Government agencies},
pages = {44--55},
}
@inproceedings{boldyreva_order-preserving_2009,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Order-{Preserving} {Symmetric} {Encryption}},
isbn = {978-3-642-01001-9},
doi = {10.1007/978-3-642-01001-9_13},
abstract = {We initiate the cryptographic study of order-preserving symmetric encryption (OPE), a primitive suggested in the database community by Agrawal et al. (SIGMOD ’04) for allowing efficient range queries on encrypted data. Interestingly, we first show that a straightforward relaxation of standard security notions for encryption such as indistinguishability against chosen-plaintext attack (IND-CPA) is unachievable by a practical OPE scheme. Instead, we propose a security notion in the spirit of pseudorandom functions (PRFs) and related primitives asking that an OPE scheme look “as-random-as-possible” subject to the order-preserving constraint. We then design an efficient OPE scheme and prove its security under our notion based on pseudorandomness of an underlying blockcipher. Our construction is based on a natural relation we uncover between a random order-preserving function and the hypergeometric probability distribution. In particular, it makes black-box use of an efficient sampling algorithm for the latter.},
language = {en},
booktitle = {Advances in {Cryptology} - {EUROCRYPT} 2009},
publisher = {Springer},
author = {Boldyreva, Alexandra and Chenette, Nathan and Lee, Younho and O’Neill, Adam},
editor = {Joux, Antoine},
year = {2009},
keywords = {Encrypt Data, Encryption Algorithm, Range Query, Sampling Algorithm, Symmetric Encryption},
pages = {224--241},
}
@article{bonawitz_towards_2019,
title = {Towards {Federated} {Learning} at {Scale}: {System} {Design}},
volume = {1},
shorttitle = {Towards {Federated} {Learning} at {Scale}},
url = {https://proceedings.mlsys.org/paper/2019/hash/bd686fd640be98efaae0091fa301e613-Abstract.html},
language = {en},
urldate = {2022-02-28},
journal = {Proceedings of Machine Learning and Systems},
author = {Bonawitz, Keith and Eichner, Hubert and Grieskamp, Wolfgang and Huba, Dzmitry and Ingerman, Alex and Ivanov, Vladimir and Kiddon, Chloé and Konečný, Jakub and Mazzocchi, Stefano and McMahan, Brendan and Van Overveldt, Timon and Petrou, David and Ramage, Daniel and Roselander, Jason},
month = apr,
year = {2019},
pages = {374--388},
}
@article{hunt_ryoan_2018,
title = {Ryoan: {A} {Distributed} {Sandbox} for {Untrusted} {Computation} on {Secret} {Data}},
volume = {35},
issn = {0734-2071},
shorttitle = {Ryoan},
url = {https://doi.org/10.1145/3231594},
doi = {10.1145/3231594},
abstract = {Users of modern data-processing services such as tax preparation or genomic screening are forced to trust them with data that the users wish to keep secret. Ryoan1 protects secret data while it is processed by services that the data owner does not trust. Accomplishing this goal in a distributed setting is difficult, because the user has no control over the service providers or the computational platform. Confining code to prevent it from leaking secrets is notoriously difficult, but Ryoan benefits from new hardware and a request-oriented data model. Ryoan provides a distributed sandbox, leveraging hardware enclaves (e.g., Intel’s software guard extensions (SGX) [40]) to protect sandbox instances from potentially malicious computing platforms. The protected sandbox instances confine untrusted data-processing modules to prevent leakage of the user’s input data. Ryoan is designed for a request-oriented data model, where confined modules only process input once and do not persist state about the input. We present the design and prototype implementation of Ryoan and evaluate it on a series of challenging problems including email filtering, health analysis, image processing and machine translation.},
number = {4},
urldate = {2022-02-28},
journal = {ACM Transactions on Computer Systems},
author = {Hunt, Tyler and Zhu, Zhiting and Xu, Yuanzhong and Peter, Simon and Witchel, Emmett},
month = dec,
year = {2018},
keywords = {Intel SGX, enclaves, private computation, sandboxing, untrusted OS},
pages = {13:1--13:32},
}
@inproceedings{popa_cryptdb_2011,
address = {New York, NY, USA},
series = {{SOSP} '11},
title = {{CryptDB}: protecting confidentiality with encrypted query processing},
isbn = {978-1-4503-0977-6},
shorttitle = {{CryptDB}},
url = {https://doi.org/10.1145/2043556.2043566},
doi = {10.1145/2043556.2043566},
abstract = {Online applications are vulnerable to theft of sensitive information because adversaries can exploit software bugs to gain access to private data, and because curious or malicious administrators may capture and leak data. CryptDB is a system that provides practical and provable confidentiality in the face of these attacks for applications backed by SQL databases. It works by executing SQL queries over encrypted data using a collection of efficient SQL-aware encryption schemes. CryptDB can also chain encryption keys to user passwords, so that a data item can be decrypted only by using the password of one of the users with access to that data. As a result, a database administrator never gets access to decrypted data, and even if all servers are compromised, an adversary cannot decrypt the data of any user who is not logged in. An analysis of a trace of 126 million SQL queries from a production MySQL server shows that CryptDB can support operations over encrypted data for 99.5\% of the 128,840 columns seen in the trace. Our evaluation shows that CryptDB has low overhead, reducing throughput by 14.5\% for phpBB, a web forum application, and by 26\% for queries from TPC-C, compared to unmodified MySQL. Chaining encryption keys to user passwords requires 11--13 unique schema annotations to secure more than 20 sensitive fields and 2--7 lines of source code changes for three multi-user web applications.},
urldate = {2022-02-28},
booktitle = {Proceedings of the {Twenty}-{Third} {ACM} {Symposium} on {Operating} {Systems} {Principles}},
publisher = {Association for Computing Machinery},
author = {Popa, Raluca Ada and Redfield, Catherine M. S. and Zeldovich, Nickolai and Balakrishnan, Hari},
month = oct,
year = {2011},
pages = {85--100},
}
@article{dean_mapreduce_2004,
title = {{MapReduce}: {Simplified} data processing on large clusters},
author = {Dean, Jeffrey and Ghemawat, Sanjay},
year = {2004},
}
@inproceedings{malewicz_pregel_2010,
address = {New York, NY, USA},
series = {{SIGMOD} '10},
title = {Pregel: a system for large-scale graph processing},
isbn = {978-1-4503-0032-2},
shorttitle = {Pregel},
url = {https://doi.org/10.1145/1807167.1807184},
doi = {10.1145/1807167.1807184},
abstract = {Many practical computing problems concern large graphs. Standard examples include the Web graph and various social networks. The scale of these graphs - in some cases billions of vertices, trillions of edges - poses challenges to their efficient processing. In this paper we present a computational model suitable for this task. Programs are expressed as a sequence of iterations, in each of which a vertex can receive messages sent in the previous iteration, send messages to other vertices, and modify its own state and that of its outgoing edges or mutate graph topology. This vertex-centric approach is flexible enough to express a broad set of algorithms. The model has been designed for efficient, scalable and fault-tolerant implementation on clusters of thousands of commodity computers, and its implied synchronicity makes reasoning about programs easier. Distribution-related details are hidden behind an abstract API. The result is a framework for processing large graphs that is expressive and easy to program.},
urldate = {2022-02-21},
booktitle = {Proceedings of the 2010 {ACM} {SIGMOD} {International} {Conference} on {Management} of data},
publisher = {Association for Computing Machinery},
author = {Malewicz, Grzegorz and Austern, Matthew H. and Bik, Aart J.C and Dehnert, James C. and Horn, Ilan and Leiser, Naty and Czajkowski, Grzegorz},
month = jun,
year = {2010},
keywords = {distributed computing, graph algorigthms},
pages = {135--146},
}
@article{isard_dryad_2007,
title = {Dryad: distributed data-parallel programs from sequential building blocks},
volume = {41},
issn = {0163-5980},
shorttitle = {Dryad},
url = {https://doi.org/10.1145/1272998.1273005},
doi = {10.1145/1272998.1273005},
abstract = {Dryad is a general-purpose distributed execution engine for coarse-grain data-parallel applications. A Dryad application combines computational "vertices" with communication "channels" to form a dataflow graph. Dryad runs the application by executing the vertices of this graph on a set of available computers, communicating as appropriate through flies, TCP pipes, and shared-memory FIFOs. The vertices provided by the application developer are quite simple and are usually written as sequential programs with no thread creation or locking. Concurrency arises from Dryad scheduling vertices to run simultaneously on multiple computers, or on multiple CPU cores within a computer. The application can discover the size and placement of data at run time, and modify the graph as the computation progresses to make efficient use of the available resources. Dryad is designed to scale from powerful multi-core single computers, through small clusters of computers, to data centers with thousands of computers. The Dryad execution engine handles all the difficult problems of creating a large distributed, concurrent application: scheduling the use of computers and their CPUs, recovering from communication or computer failures, and transporting data between vertices.},
number = {3},
urldate = {2022-02-21},
journal = {ACM SIGOPS Operating Systems Review},
author = {Isard, Michael and Budiu, Mihai and Yu, Yuan and Birrell, Andrew and Fetterly, Dennis},
month = mar,
year = {2007},
keywords = {cluster computing, concurrency, dataflow, distributed programming},
pages = {59--72},
}
@misc{noauthor_osdi_nodate,
title = {{OSDI} '04 {Abstract}},
url = {https://www.usenix.org/legacy/events/osdi04/tech/dean.html},
urldate = {2022-02-21},
}
@article{dean_mapreduce_2008,
title = {{MapReduce}: simplified data processing on large clusters},
volume = {51},
issn = {0001-0782},
shorttitle = {{MapReduce}},
url = {https://doi.org/10.1145/1327452.1327492},
doi = {10.1145/1327452.1327492},
abstract = {MapReduce is a programming model and an associated implementation for processing and generating large datasets that is amenable to a broad variety of real-world tasks. Users specify the computation in terms of a map and a reduce function, and the underlying runtime system automatically parallelizes the computation across large-scale clusters of machines, handles machine failures, and schedules inter-machine communication to make efficient use of the network and disks. Programmers find the system easy to use: more than ten thousand distinct MapReduce programs have been implemented internally at Google over the past four years, and an average of one hundred thousand MapReduce jobs are executed on Google's clusters every day, processing a total of more than twenty petabytes of data per day.},
number = {1},
urldate = {2022-02-21},
journal = {Communications of the ACM},
author = {Dean, Jeffrey and Ghemawat, Sanjay},
month = jan,
year = {2008},
pages = {107--113},
}
@article{hindman_mesos_nodate,
title = {Mesos: {A} {Platform} for {Fine}-{Grained} {Resource} {Sharing} in the {Data} {Center}},
abstract = {We present Mesos, a platform for sharing commodity clusters between multiple diverse cluster computing frameworks, such as Hadoop and MPI. Sharing improves cluster utilization and avoids per-framework data replication. Mesos shares resources in a fine-grained manner, allowing frameworks to achieve data locality by taking turns reading data stored on each machine. To support the sophisticated schedulers of today’s frameworks, Mesos introduces a distributed two-level scheduling mechanism called resource offers. Mesos decides how many resources to offer each framework, while frameworks decide which resources to accept and which computations to run on them. Our results show that Mesos can achieve near-optimal data locality when sharing the cluster among diverse frameworks, can scale to 50,000 (emulated) nodes, and is resilient to failures.},
language = {en},
author = {Hindman, Benjamin and Konwinski, Andy and Zaharia, Matei and Ghodsi, Ali and Joseph, Anthony D and Katz, Randy and Shenker, Scott and Stoica, Ion},
pages = {14},
}
@article{delimitrou_quasar_nodate,
title = {Quasar: {Resource}-{Efficient} and {QoS}-{Aware} {Cluster} {Management}},
abstract = {Cloud computing promises flexibility and high performance for users and high cost-efficiency for operators. Nevertheless, most cloud facilities operate at very low utilization, hurting both cost effectiveness and future scalability.},
language = {en},
author = {Delimitrou, Christina and Kozyrakis, Christos},
pages = {17},
}
@inproceedings{gog_firmament_2016,
title = {Firmament: {Fast}, {Centralized} {Cluster} {Scheduling} at {Scale}},
isbn = {978-1-931971-33-1},
shorttitle = {Firmament},
url = {https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gog},
language = {en},
urldate = {2022-02-14},
author = {Gog, Ionel and Schwarzkopf, Malte and Gleave, Adam and Watson, Robert N. M. and Hand, Steven},
year = {2016},
pages = {99--115},
}
@misc{zhang_fuxi_2014,
type = {Proceedings {Paper}},
title = {Fuxi: {A} fault-tolerant resource management and job scheduling system at internet scale},
copyright = {cc\_by\_nc\_nd\_4},
shorttitle = {Fuxi},
url = {http://www.vldb.org/pvldb/vol7/p1393-zhang.pdf},
abstract = {Scalability and fault-tolerance are two fundamental challenges for all distributed computing at Internet scale. Despite many recent advances from both academia and industry, these two problems are still far from settled. In this paper, we present Fuxi, a resource management and job scheduling system that is capable of handling the kind of workload at Alibaba where hundreds of terabytes of data are generated and analyzed everyday to help optimize the company's business operations and user experiences. We employ several novel techniques to enable Fuxi to perform efficient scheduling of hundreds of thousands of concurrent tasks over large clusters with thousands of nodes: 1) an incremental resource management protocol that supports multi-dimensional resource allocation and data locality; 2) user-transparent failure recovery where failures of any Fuxi components will not impact the execution of user jobs; and 3) an effective detection mechanism and a multi-level blacklisting scheme that prevents them from affecting job execution. Our evaluation results demonstrate that 95\% and 91\% scheduled CPU/memory utilization can be fulfilled under synthetic workloads, and Fuxi is capable of achieving 2.36T-B/minute throughput in GraySort. Additionally, the same Fuxi job only experiences approximately 16\% slowdown under a 5\% fault-injection rate. The slowdown only grows to 20\% when we double the fault-injection rate to 10\%. Fuxi has been deployed in our production environment since 2009, and it now manages hundreds of thousands of server nodes.},
language = {en},
urldate = {2022-02-14},
journal = {Proceedings of the VLDB Endowment},
author = {Zhang, Z. and Li, C. and Tao, Y. and Yang, R. and Tang, H. and Xu, J.},
month = aug,
year = {2014},
note = {Conference Name: 40th International Conference on Very Large Data Bases
ISSN: 2150-8097
Issue: 13
Meeting Name: 40th International Conference on Very Large Data Bases
Number: 13
Pages: 1393-1404
Place: Hangzhou, China
Publisher: VLDB Endowment Inc.
Volume: 7},
}
@inproceedings{verma_large-scale_2015,
address = {New York, NY, USA},
series = {{EuroSys} '15},
title = {Large-scale cluster management at {Google} with {Borg}},
isbn = {978-1-4503-3238-5},
url = {https://doi.org/10.1145/2741948.2741964},
doi = {10.1145/2741948.2741964},
abstract = {Google's Borg system is a cluster manager that runs hundreds of thousands of jobs, from many thousands of different applications, across a number of clusters each with up to tens of thousands of machines. It achieves high utilization by combining admission control, efficient task-packing, over-commitment, and machine sharing with process-level performance isolation. It supports high-availability applications with runtime features that minimize fault-recovery time, and scheduling policies that reduce the probability of correlated failures. Borg simplifies life for its users by offering a declarative job specification language, name service integration, real-time job monitoring, and tools to analyze and simulate system behavior. We present a summary of the Borg system architecture and features, important design decisions, a quantitative analysis of some of its policy decisions, and a qualitative examination of lessons learned from a decade of operational experience with it.},
urldate = {2022-02-14},
booktitle = {Proceedings of the {Tenth} {European} {Conference} on {Computer} {Systems}},
publisher = {Association for Computing Machinery},
author = {Verma, Abhishek and Pedrosa, Luis and Korupolu, Madhukar and Oppenheimer, David and Tune, Eric and Wilkes, John},
month = apr,
year = {2015},
pages = {1--17},
}
@article{sewell_x86-tso_2010,
title = {x86-{TSO}: a rigorous and usable programmer's model for x86 multiprocessors},
volume = {53},
issn = {0001-0782},
shorttitle = {x86-{TSO}},
url = {https://doi.org/10.1145/1785414.1785443},
doi = {10.1145/1785414.1785443},
abstract = {Exploiting the multiprocessors that have recently become ubiquitous requires high-performance and reliable concurrent systems code, for concurrent data structures, operating system kernels, synchronization libraries, compilers, and so on. However, concurrent programming, which is always challenging, is made much more so by two problems. First, real multiprocessors typically do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, varying in subtle ways between processor families, in which different hardware threads may have only loosely consistent views of a shared memory. Second, the public vendor architectures, supposedly specifying what programmers can rely on, are often in ambiguous informal prose (a particularly poor medium for loose specifications), leading to widespread confusion. In this paper we focus on x86 processors. We review several recent Intel and AMD specifications, showing that all contain serious ambiguities, some are arguably too weak to program above, and some are simply unsound with respect to actual hardware. We present a new x86-TSO programmer's model that, to the best of our knowledge, suffers from none of these problems. It is mathematically precise (rigorously defined in HOL4) but can be presented as an intuitive abstract machine which should be widely accessible to working programmers. We illustrate how this can be used to reason about the correctness of a Linux spinlock implementation and describe a general theory of data-race freedom for x86-TSO. This should put x86 multiprocessor system building on a more solid foundation; it should also provide a basis for future work on verification of such systems.},
number = {7},
urldate = {2022-02-10},
journal = {Communications of the ACM},
author = {Sewell, Peter and Sarkar, Susmit and Owens, Scott and Nardelli, Francesco Zappa and Myreen, Magnus O.},
month = jul,
year = {2010},
pages = {89--97},
}
@article{hunt_zookeeper_2010,
title = {{ZooKeeper}: {Wait}-free coordination for {Internet}-scale systems},
abstract = {In this paper, we describe ZooKeeper, a service for coordinating processes of distributed applications. Since ZooKeeper is part of critical infrastructure, ZooKeeper aims to provide a simple and high performance kernel for building more complex coordination primitives at the client. It incorporates elements from group messaging, shared registers, and distributed lock services in a replicated, centralized service. The interface exposed by ZooKeeper has the wait-free aspects of shared registers with an event-driven mechanism similar to cache invalidations of distributed file systems to provide a simple, yet powerful coordination service.},
language = {en},
author = {Hunt, Patrick and Konar, Mahadev and Junqueira, Flavio P and Reed, Benjamin},
year = {2010},
pages = {14},
}
@article{van_renesse_paxos_2015,
title = {Paxos {Made} {Moderately} {Complex}},
volume = {47},
issn = {0360-0300},
url = {https://doi.org/10.1145/2673577},
doi = {10.1145/2673577},
abstract = {This article explains the full reconfigurable multidecree Paxos (or multi-Paxos) protocol. Paxos is by no means a simple protocol, even though it is based on relatively simple invariants. We provide pseudocode and explain it guided by invariants. We initially avoid optimizations that complicate comprehension. Next we discuss liveness, list various optimizations that make the protocol practical, and present variants of the protocol.},
number = {3},
urldate = {2022-02-07},
journal = {ACM Computing Surveys},
author = {Van Renesse, Robbert and Altinbuken, Deniz},
month = feb,
year = {2015},
keywords = {Replicated state machines, consensus, voting},
pages = {42:1--42:36},
}
@inproceedings{burrows_chubby_2006,
address = {USA},
series = {{OSDI} '06},
title = {The {Chubby} lock service for loosely-coupled distributed systems},
isbn = {978-1-931971-47-8},
abstract = {We describe our experiences with the Chubby lock service, which is intended to provide coarse-grained locking as well as reliable (though low-volume) storage for a loosely-coupled distributed system. Chubby provides an interface much like a distributed file system with advisory locks, but the design emphasis is on availability and reliability, as opposed to high performance. Many instances of the service have been used for over a year, with several of them each handling a few tens of thousands of clients concurrently. The paper describes the initial design and expected use, compares it with actual use, and explains how the design had to be modified to accommodate the differences.},
urldate = {2022-02-07},
booktitle = {Proceedings of the 7th symposium on {Operating} systems design and implementation},
publisher = {USENIX Association},
author = {Burrows, Mike},
month = nov,
year = {2006},
pages = {335--350},
}
@inproceedings{ongaro_search_2014,
title = {In {Search} of an {Understandable} {Consensus} {Algorithm}},
isbn = {978-1-931971-10-2},
url = {https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro},
language = {en},
urldate = {2022-02-07},
author = {Ongaro, Diego and Ousterhout, John},
year = {2014},
pages = {305--319},
}
@misc{the_docker_team_its_2014,
title = {It’s {Here}: {Docker} 1.0 {\textbar} {Docker} {Blog}},
shorttitle = {It’s {Here}},
url = {https://blog.docker.com/2014/06/its-here-docker-1-0/},
urldate = {2014-06-11},
author = {The Docker Team},
month = jun,
year = {2014},
}
@article{yasunori_kernel-based_2011,
title = {Kernel-based {Virtual} {Machine} {Technology}},
volume = {47},
language = {en},
number = {3},
journal = {FUJITSU Sci. Tech. J.},
author = {Yasunori, Goto},
year = {2011},
pages = {7},
}
@misc{hamilton_xen--nitro_nodate,
type = {Blog},
title = {Xen-on-{Nitro}: {AWS} {Nitro} for {Legacy} {Instances} – {Perspectives}},
shorttitle = {Xen-on-{Nitro}},
url = {https://perspectives.mvdirona.com/2021/11/xen-on-nitro-aws-nitro-for-legacy-instances/},
language = {en-US},
urldate = {2022-02-03},
journal = {Perspectives},
author = {Hamilton, James},
}
@article{duda_borrowed-virtual-time_1999,
title = {Borrowed-virtual-time ({BVT}) scheduling: supporting latency-sensitive threads in a general-purpose scheduler},
volume = {33},
issn = {0163-5980},
shorttitle = {Borrowed-virtual-time ({BVT}) scheduling},
url = {https://doi.org/10.1145/319344.319169},
doi = {10.1145/319344.319169},
abstract = {Systems need to run a larger and more diverse set of applications, from real-time to interactive to batch, on uniprocessor and multiprocessor platforms. However, most schedulers either do not address latency requirements or are specialized to complex real-time paradigms, limiting their applicability to general-purpose systems.In this paper, we present Borrowed-Virtual-Time (BVT) Scheduling, showing that it provides low-latency for real-time and interactive applications yet weighted sharing of the CPU across applications according to system policy, even with thread failure at the real-time level, all with a low-overhead implementation on multiprocessors as well as uniprocessors. It makes minimal demands on application developers, and can be used with a reservation or admission control module for hard real-time applications.},
number = {5},
urldate = {2022-02-03},
journal = {ACM SIGOPS Operating Systems Review},
author = {Duda, Kenneth J. and Cheriton, David R.},
month = dec,
year = {1999},
pages = {261--276},
}
@techreport{vmware_inc_understanding_2008,
title = {Understanding {Full} {Virtualization}, {Paravirtualization} and {Hardware} {Assist}},
url = {https://www.vmware.com/content/dam/digitalmarketing/vmware/en/pdf/techpaper/VMware_paravirtualization.pdf},
abstract = {In 1998, VMware figured out how to virtualize the x86 platform, once thought to be impossible, and created the market for x86 virtualization. The solution was a combination of binary translation and direct execution on the processor that allowed multiple guest OSes to run in full isolation on the same computer with readily affordable virtualization overhead.The savings that tens of thousands of companies have generated from the deployment of this technology is further driving the rapid adoption of virtualized computing from the desktop to the data center. As new vendors enter the space and attempt to differentiate their products, many are creating confusion with their marketing claims and terminology. For example, while hardware assist is a valuable technique that will mature and expand the envelope of workloads that can be virtualized, paravirtualization is not an entirely new technology that offers an order ofmagnitude greater performance.While this is a complex and rapidly evolving space, the technologies employed can be readily explained to help companies understand their options and choose a path forward. This white paper attempts to clarify the various techniques used to virtualize x86 hardware, the strengths and weaknesses of each, and VMware™s community approach to develop and employ the most effective of the emerging virtualization techniques. Figure 1 provides a summary timeline of x86virtualization technologies from VMware™s binary translation to the recent application of kernel paravirtualization and hardware-assisted virtualization.},
urldate = {2022-02-02},
author = {VMware, Inc.},
month = mar,
year = {2008},
}
@inproceedings{litton_light-weight_2016,
title = {\{{Light}-{Weight}\} {Contexts}: {An} \{{OS}\} {Abstraction} for {Safety} and {Performance}},
isbn = {978-1-931971-33-1},
shorttitle = {\{{Light}-{Weight}\} {Contexts}},
url = {https://www.usenix.org/conference/osdi16/technical-sessions/presentation/litton},
language = {en},
urldate = {2022-01-31},
author = {Litton, James and Vahldiek-Oberwagner, Anjo and Elnikety, Eslam and Garg, Deepak and Bhattacharjee, Bobby and Druschel, Peter},
year = {2016},
pages = {49--64},
}
@inproceedings{manco_my_2017,
address = {New York, NY, USA},
series = {{SOSP} '17},
title = {My {VM} is {Lighter} (and {Safer}) than your {Container}},
isbn = {978-1-4503-5085-3},
url = {https://doi.org/10.1145/3132747.3132763},
doi = {10.1145/3132747.3132763},
abstract = {Containers are in great demand because they are lightweight when compared to virtual machines. On the downside, containers offer weaker isolation than VMs, to the point where people run containers in virtual machines to achieve proper isolation. In this paper, we examine whether there is indeed a strict tradeoff between isolation (VMs) and efficiency (containers). We find that VMs can be as nimble as containers, as long as they are small and the toolstack is fast enough. We achieve lightweight VMs by using unikernels for specialized applications and with Tinyx, a tool that enables creating tailor-made, trimmed-down Linux virtual machines. By themselves, lightweight virtual machines are not enough to ensure good performance since the virtualization control plane (the toolstack) becomes the performance bottleneck. We present LightVM, a new virtualization solution based on Xen that is optimized to offer fast boot-times regardless of the number of active VMs. LightVM features a complete redesign of Xen's control plane, transforming its centralized operation to a distributed one where interactions with the hypervisor are reduced to a minimum. LightVM can boot a VM in 2.3ms, comparable to fork/exec on Linux (1ms), and two orders of magnitude faster than Docker. LightVM can pack thousands of LightVM guests on modest hardware with memory and CPU usage comparable to that of processes.},
urldate = {2022-01-31},
booktitle = {Proceedings of the 26th {Symposium} on {Operating} {Systems} {Principles}},
publisher = {Association for Computing Machinery},
author = {Manco, Filipe and Lupu, Costin and Schmidt, Florian and Mendes, Jose and Kuenzer, Simon and Sati, Sumit and Yasukata, Kenichi and Raiciu, Costin and Huici, Felipe},
month = oct,
year = {2017},
keywords = {Virtualization, Xen, containers, hypervisor, operating systems, specialization, unikernels, virtual machine},
pages = {218--233},
}
@inproceedings{soltesz_container-based_2007,
address = {New York, NY, USA},
series = {{EuroSys} '07},
title = {Container-based operating system virtualization: a scalable, high-performance alternative to hypervisors},
isbn = {978-1-59593-636-3},
shorttitle = {Container-based operating system virtualization},
url = {https://doi.org/10.1145/1272996.1273025},
doi = {10.1145/1272996.1273025},
abstract = {Hypervisors, popularized by Xen and VMware, are quickly becoming commodity. They are appropriate for many usage scenarios, but there are scenarios that require system virtualization with high degrees of both isolation and efficiency. Examples include HPC clusters, the Grid, hosting centers, and PlanetLab. We present an alternative to hypervisors that is better suited to such scenarios. The approach is a synthesis of prior work on resource containers and security containers applied to general-purpose, time-shared operating systems. Examples of such container-based systems include Solaris 10, Virtuozzo for Linux, and Linux-VServer. As a representative instance of container-based systems, this paper describes the design and implementation of Linux-VServer. In addition, it contrasts the architecture of Linux-VServer with current generations of Xen, and shows how Linux-VServer provides comparable support for isolation and superior system efficiency.},
urldate = {2022-01-31},
booktitle = {Proceedings of the 2nd {ACM} {SIGOPS}/{EuroSys} {European} {Conference} on {Computer} {Systems} 2007},
publisher = {Association for Computing Machinery},
author = {Soltesz, Stephen and Pötzl, Herbert and Fiuczynski, Marc E. and Bavier, Andy and Peterson, Larry},
month = mar,
year = {2007},
keywords = {Linux-VServer, Xen, alternative, container, hypervisor, operating, system, virtualization},
pages = {275--287},
}
@article{barham_xen_2003,
title = {Xen and the art of virtualization},
volume = {37},
issn = {0163-5980},
url = {https://doi.org/10.1145/1165389.945462},
doi = {10.1145/1165389.945462},
abstract = {Numerous systems have been designed which use virtualization to subdivide the ample resources of a modern computer. Some require specialized hardware, or cannot support commodity operating systems. Some target 100\% binary compatibility at the expense of performance. Others sacrifice security or functionality for speed. Few offer resource isolation or performance guarantees; most provide only best-effort provisioning, risking denial of service.This paper presents Xen, an x86 virtual machine monitor which allows multiple commodity operating systems to share conventional hardware in a safe and resource managed fashion, but without sacrificing either performance or functionality. This is achieved by providing an idealized virtual machine abstraction to which operating systems such as Linux, BSD and Windows XP, can be ported with minimal effort.Our design is targeted at hosting up to 100 virtual machine instances simultaneously on a modern server. The virtualization approach taken by Xen is extremely efficient: we allow operating systems such as Linux and Windows XP to be hosted simultaneously for a negligible performance overhead --- at most a few percent compared with the unvirtualized case. We considerably outperform competing commercial and freely available solutions in a range of microbenchmarks and system-wide tests.},
number = {5},
urldate = {2022-01-31},
journal = {ACM SIGOPS Operating Systems Review},
author = {Barham, Paul and Dragovic, Boris and Fraser, Keir and Hand, Steven and Harris, Tim and Ho, Alex and Neugebauer, Rolf and Pratt, Ian and Warfield, Andrew},
month = oct,
year = {2003},
keywords = {hypervisors, paravirtualization, virtual machine monitors},
pages = {164--177},
}
@article{ritchie_unix_1974,
title = {The {UNIX} time-sharing system},
volume = {17},
issn = {0001-0782},
url = {https://doi.org/10.1145/361011.361061},
doi = {10.1145/361011.361061},
abstract = {UNIX is a general-purpose, multi-user, interactive operating system for the Digital Equipment Corporation PDP-11/40 and 11/45 computers. It offers a number of features seldom found even in larger operating systems, including: (1) a hierarchical file system incorporating demountable volumes; (2) compatible file, device, and inter-process I/O; (3) the ability to initiate asynchronous processes; (4) system command language selectable on a per-user basis; and (5) over 100 subsystems including a dozen languages. This paper discusses the nature and implementation of the file system and of the user command interface.},
number = {7},
urldate = {2022-01-24},
journal = {Communications of the ACM},
author = {Ritchie, Dennis M. and Thompson, Ken},
month = jul,
year = {1974},
keywords = {PDP-11, command language, file system, operating system, time-sharing},
pages = {365--375},
}
@article{madhavapeddy_unikernels_2013,
title = {Unikernels: library operating systems for the cloud},
volume = {41},
issn = {0163-5964},
shorttitle = {Unikernels},
url = {https://doi.org/10.1145/2490301.2451167},
doi = {10.1145/2490301.2451167},
abstract = {We present unikernels, a new approach to deploying cloud services via applications written in high-level source code. Unikernels are single-purpose appliances that are compile-time specialised into standalone kernels, and sealed against modification when deployed to a cloud platform. In return they offer significant reduction in image sizes, improved efficiency and security, and should reduce operational costs. Our Mirage prototype compiles OCaml code into unikernels that run on commodity clouds and offer an order of magnitude reduction in code size without significant performance penalty. The architecture combines static type-safety with a single address-space layout that can be made immutable via a hypervisor extension. Mirage contributes a suite of type-safe protocol libraries, and our results demonstrate that the hypervisor is a platform that overcomes the hardware compatibility issues that have made past library operating systems impractical to deploy in the real-world.},
number = {1},
urldate = {2022-01-24},
journal = {ACM SIGARCH Computer Architecture News},
author = {Madhavapeddy, Anil and Mortier, Richard and Rotsos, Charalampos and Scott, David and Singh, Balraj and Gazagnaire, Thomas and Smith, Steven and Hand, Steven and Crowcroft, Jon},
month = mar,
year = {2013},
keywords = {functional programming, hypervisor, microkernel},
pages = {461--472},
}
@inproceedings{baumann_multikernel_2009,
address = {New York, NY, USA},
series = {{SOSP} '09},
title = {The multikernel: a new {OS} architecture for scalable multicore systems},
isbn = {978-1-60558-752-3},
shorttitle = {The multikernel},
url = {https://doi.org/10.1145/1629575.1629579},
doi = {10.1145/1629575.1629579},
abstract = {Commodity computer systems contain more and more processor cores and exhibit increasingly diverse architectural tradeoffs, including memory hierarchies, interconnects, instruction sets and variants, and IO configurations. Previous high-performance computing systems have scaled in specific cases, but the dynamic nature of modern client and server workloads, coupled with the impossibility of statically optimizing an OS for all workloads and hardware variants pose serious challenges for operating system structures. We argue that the challenge of future multicore hardware is best met by embracing the networked nature of the machine, rethinking OS architecture using ideas from distributed systems. We investigate a new OS structure, the multikernel, that treats the machine as a network of independent cores, assumes no inter-core sharing at the lowest level, and moves traditional OS functionality to a distributed system of processes that communicate via message-passing. We have implemented a multikernel OS to show that the approach is promising, and we describe how traditional scalability problems for operating systems (such as memory management) can be effectively recast using messages and can exploit insights from distributed systems and networking. An evaluation of our prototype on multicore systems shows that, even on present-day machines, the performance of a multikernel is comparable with a conventional OS, and can scale better to support future hardware.},
urldate = {2022-01-24},
booktitle = {Proceedings of the {ACM} {SIGOPS} 22nd symposium on {Operating} systems principles},
publisher = {Association for Computing Machinery},
author = {Baumann, Andrew and Barham, Paul and Dagand, Pierre-Evariste and Harris, Tim and Isaacs, Rebecca and Peter, Simon and Roscoe, Timothy and Schüpbach, Adrian and Singhania, Akhilesh},
month = oct,
year = {2009},
keywords = {message passing, multicore processors, scalability},
pages = {29--44},
}
@article{engler_exokernel_1995,
title = {Exokernel: an operating system architecture for application-level resource management},
volume = {29},
issn = {0163-5980},
shorttitle = {Exokernel},
url = {https://doi.org/10.1145/224057.224076},
doi = {10.1145/224057.224076},
number = {5},
urldate = {2022-01-24},
journal = {ACM SIGOPS Operating Systems Review},
author = {Engler, D. R. and Kaashoek, M. F. and O'Toole, J.},
month = dec,
year = {1995},
pages = {251--266},
}
@inproceedings{lampson_hints_1983,
address = {New York, NY, USA},
series = {{SOSP} '83},
title = {Hints for computer system design},
isbn = {978-0-89791-115-3},
url = {https://doi.org/10.1145/800217.806614},
doi = {10.1145/800217.806614},
abstract = {Experience with the design and implementation of a number of computer systems, and study of many other systems, has led to some general hints for system design which are described here. They are illustrated by a number of examples, ranging from hardware such as the Alto and the Dorado to applications programs such as Bravo and Star.},
urldate = {2022-01-20},
booktitle = {Proceedings of the ninth {ACM} symposium on {Operating} systems principles},
publisher = {Association for Computing Machinery},
author = {Lampson, Butler W.},
month = oct,
year = {1983},
pages = {33--48},
}
@inproceedings{neumann_role_1969,
address = {New York, NY, USA},
series = {{SOSP} '69},
title = {The role of motherhood in the pop art of system programming},
isbn = {978-1-4503-7456-9},
url = {https://doi.org/10.1145/961053.961060},
doi = {10.1145/961053.961060},
abstract = {Numerous papers and conference talks have recently been devoted to the affirmation or reaffirmation of various common-sense principles of computer program design and implementation, particularly with respect to operating systems and to large subsystems such as language translators. These principles are nevertheless little observed in practice, often to the detriment of the resulting systems. This paper attempts to summarize the most significant principles, to evaluate their applicability in the real world of large multi-access systems, and to assess how they can be used more effectively.},
urldate = {2022-01-20},
booktitle = {Proceedings of the second symposium on {Operating} systems principles},
publisher = {Association for Computing Machinery},
author = {Neumann, Peter G.},
month = oct,
year = {1969},
pages = {13--18},
}
@inproceedings{needham_theory_1969,
address = {New York, NY, USA},
series = {{SOSP} '69},
title = {Theory and practice in operating system design},
isbn = {978-1-4503-7456-9},
url = {https://doi.org/10.1145/961053.961058},
doi = {10.1145/961053.961058},
abstract = {In designing an operating system one needs both theoretical insight and horse sense. Without the former, one designs an ad hoc mess; without the latter one designs an elephant in best Carrara marble (white, perfect, and immobile). We try in this paper to explore the provinces of the two needs, suggesting places where we think horse sense will always be needed, and some other places where better theoretical understanding than we now have would seem both possible and helpful.},
urldate = {2022-01-20},
booktitle = {Proceedings of the second symposium on {Operating} systems principles},
publisher = {Association for Computing Machinery},
author = {Needham, R. M. and Hartley, D. F.},
month = oct,
year = {1969},
pages = {8--12},
}
@article{ghosh_right_2020,
title = {Right buffer sizing matters: {Some} dynamical and statistical studies on {Compound} {TCP}},