Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
fediscience.org is one of the many independent Mastodon servers you can use to participate in the fediverse.
fediscience.org is a social network for scientists run by FediScience e.V., an international association dedicated to promoting scientific communication.

Administered by:

Server stats:

1.3K
active users

fediscience.org: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.0

Marc Brooker boosted
Public
Jeremy Daly

Issue #304 of Off-by-none is out! This week, AWS turns on the pre:Invent firehose, AppSync gives us better #serverless WebSockets, and Neon simplifies row-level security. Plus, we recognize Marc Brooker as our ️ of the week! #offbynone offbynone.io/issues/304/

offbynone.ioYou get to drink... from the firehose 🚒 - Off-by-noneIn this issue, AWS turns on the pre:Invent announcement firehose, AppSync gives us better serverless WebSockets, and Neon simplifies row-level security for Postgres.
Public
Marc Brooker

I'm on the AWS Developers podcast this morning, talking to Julian Wood about AWS Lambda's 10th anniversary, the growth of serverless, and some of what we learned along the way.

developers.podcast.go-aws.com/

AWS Developers Podcast · AWS Lambda: A Decade of TransformationIn this episode of the AWS Developers Podcast, Julian Wood hosts a discussion with Marc Brooker, a distinguished engineer involved in the creation of AWS Lambda. They explore the origins of Lambda, its evolution, and the impact of serverless technology on modern computing. The conversation delves into customer-centric innovations, the challenges of event-driven architectures, and the future of serverless in the context of generative AI. Mark reflects on the journey of Lambda, the lessons learned, and the exciting possibilities that lie ahead for serverless technology.
Continued thread
Public
Marc Brooker

"But what about time-to-market?" has been one of the objections to automated reasoning and formal methods forever, but in many domains they allow us to get to market faster. This is especially true in security, availability, and durability-critical domains.

Public
Marc Brooker

Great new piece from Byron Cook about automated reasoning at AWS, and how we're finding it not only allows us to deliver safer code, but also deliver faster code, and deliver code faster. aws.amazon.com/blogs/security/

Amazon Web Services · An unexpected discovery: Automated reasoning often makes systems more efficient and easier to maintain | Amazon Web ServicesDuring a recent visit to the Defense Advanced Research Projects Agency (DARPA), I mentioned a trend that piqued their interest: Over the last 10 years of applying automated reasoning at Amazon Web Services (AWS), we’ve found that formally verified code is often more performant than the unverified code it replaces. The reason is that the […]
Marc Brooker boosted
Public
Jonathan Yu

"In practice, the redundant nature of connectivity and ability to use routing mechanisms to send clients to the healthy side of partitions means that the vast majority of cloud systems can offer both strong consistency and high availability to their clients, even in the presence of the most common types of network partitions (and other failures)."

brooker.co.za/blog/2024/07/25/ by @marcbrooker

brooker.co.zaLet's Consign CAP to the Cabinet of Curiosities - Marc's Blog
Marc Brooker boosted
Public
Jonathan Yu

"Increasing memory pressure increases the amount of time it takes for the GC to run, and increases the cost of handling any given request, this increases per-request latency and reduces throughput, this increases the number of requests in flight (and their associated per-request memory), which increases memory pressure."

"[W]ith some collectors, the cost of performing a unit of work can increase by up to 70% as memory pressure increases."

brooker.co.za/blog/2024/08/14/ by @marcbrooker

brooker.co.zaGarbage Collection and Metastability - Marc's Blog
Marc Brooker<p>More great work from Kyle, and another reminder that retrying isn&#39;t the safe best-practice that many folks assume it is: <a href="https://jepsen.io/analyses/jetcd-0.8.2" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">jepsen.io/analyses/jetcd-0.8.2</span><span class="invisible"></span></a></p>
Marc Brooker<p>I&#39;ve been learning Lean recently to add to my formal toolkit, and it&#39;s been a really eye-opening experience. I don&#39;t have much of a math background, but have already found Lean lets me do things that I found really hard before.</p>
Marc Brooker<p>Loved this talk by Terence Tao on math, AI, and proof assistants. I suspect we&#39;re going to see a similar effect in software: AI will allow formal specs to be developed faster than traditional programs, and for programs to be generated from those specs. <a href="https://www.youtube.com/watch?v=_sTDSO74D8Q" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=_sTDSO74D8</span><span class="invisible">Q</span></a></p>
Marc Brooker<p>So much fun systems work here. I&#39;m super proud of the team that shipped this product, and wrote this paper describing (a small part of) their innovation. Check out our paper here: <a href="https://www.amazon.science/publications/resource-management-in-aurora-serverless" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">amazon.science/publications/re</span><span class="invisible">source-management-in-aurora-serverless</span></a></p>
Marc Brooker<p>Next, we had to learn how to actively manage heat across the database fleet, in a way that ensured the right resources are available when customers need them. This work included placement, live migration, and instance-level controls.</p>
Marc Brooker<p>Next, we had to place databases across a large fleet in a way that allowed us to optimize for performance, predictability, and cost. Placement allows us to pick workloads that fit nicely together, such as by wanting to scale at different times.</p>
Marc Brooker<p>Teaching database engines how to scale up isn&#39;t too hard: they&#39;re hungry hippos and will eat all the memory and CPU you can give them. Teaching them to scale down was harder, and required us to really understand what drives working-set behavior at the engine and OS level.</p>
Marc Brooker
Marc Brooker<p>New blog post, on our paper about Aurora Serverless V2 &quot;Resource Management in Aurora Serverless&quot;: <a href="https://brooker.co.za/blog/2024/07/29/aurora-serverless.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">brooker.co.za/blog/2024/07/29/</span><span class="invisible">aurora-serverless.html</span></a> What I loved about this project was being able to innovate at all levels of the stack, from the hypervisor all the way to region-scale clusters.</p>
Marc Brooker<p>Let&#39;s assign CAP to the cabinet of curiosities: <a href="https://brooker.co.za/blog/2024/07/25/cap-again.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">brooker.co.za/blog/2024/07/25/</span><span class="invisible">cap-again.html</span></a></p><p>If you’re an experienced distributed systems person teaching new folks about trade-offs in your space, please don’t start with CAP. Tons of more interesting, more instructive, trade-offs.</p>
Marc Brooker<p>I think the porosity on the head is caused by incomplete burnout, but not sure about the generally rough surface texture (the investment I&#39;m using should be able to do a ton better). Technically not &quot;lost PLA&quot;, but &quot;lost PVB&quot; (Polymaker Polycast). Metal is ZA-12 (zinc aluminium alloy).</p><p>This is entirely the first casting I&#39;ve done since making die-cast tin soldiers with my friend&#39;s grandfathers stuff like 30 years ago.</p>
Marc Brooker<p>First attempt at &quot;lost PLA&quot; investment casting: psyduck.</p>
Marc Brooker<p>Here&#39;s a practical example of how Formal Methods can make code faster: AWS&#39;s new proven-correct authorization engine is 65% faster (even at p99.9) than the previous version. </p><p><a href="https://youtu.be/oshxAJGrwMU?si=3kjRoUIaa527u3EI&amp;t=3188" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">youtu.be/oshxAJGrwMU?si=3kjRoU</span><span class="invisible">Iaa527u3EI&amp;t=3188</span></a></p><p>Sean says in the talk &quot;we wouldn&#39;t have attempted a lot of optimizations we did without this backing of proof&quot;.</p><p>Formal methods allow us to optimize systems more boldly, by removing the risk that optimizations will affect correctness.</p>
Marc Brooker<p>This is super cool: researchers at @UW using time domain reflectometry in existing teleco optic fibers to measure seismic activity at Mt Rainier: <a href="https://www.youtube.com/watch?v=3E5N9B2xpOU" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=3E5N9B2xpO</span><span class="invisible">U</span></a> As far as I can tell what they&#39;re looking at here is variations in Rayleigh scattering of light inside the fiber. Rayleigh scattering is proportional to the eighth power of refractive index, which makes this technique super sensitive to even small changes in the index.</p>
Marc Brooker<p>Fascinating: the Cascades Volcano Observatory&#39;s seismic monitoring of Mt Rainier is sensitive enough to track avalanches: <a href="https://www.youtube.com/watch?v=HyTTSDXrPcY" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=HyTTSDXrPc</span><span class="invisible">Y</span></a> (but they&#39;re looking for something much bigger: lahars).</p>
Marc Brooker<p>This kind of research is interesting to me, as a practitioner, because correctness is one of the hardest things we do. Finding new ways to reason about the correctness of systems is super valuable to us - both in saving development time and in building better systems.</p>
Marc Brooker<p>The core idea behind their approach is rather simple: two &quot;facts&quot; about operations encoded in their types.</p>
Marc Brooker<p>I especially like how they&#39;ve combined three approaches (their type-based approach, model checking in Alloy, and classic testing approaches) to find implementation bugs at multiple different levels. This is exactly the approach to verification and testing I recommend at AWS.</p>
Marc Brooker<p>Crash consistency matters for filesystems and databases because, without it, it&#39;s impossible for the FS or DB to provide guarantees that extend beyond unplanned system reboots. Unplanned reboots do happen, and so this is a critical real-world property.</p>
Marc Brooker<p>This SquirrelFS paper by Hayley LeBlanc et al is extremely cool. The short version is that they use the Typestate pattern (along with Rust&#39;s type checker) to check certain crash consistency properties of a filesystem *at compile time*. Check out their paper at <a href="https://arxiv.org/abs/2406.09649" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2406.09649</span><span class="invisible"></span></a> (and I think they&#39;re at OSDI this week too).</p>
Marc Brooker<p>New post on my misc blog, suggesting a way to make the Prusa XL a much better printer: <a href="https://brooker.co.za/misc-blog/2024/07/07/prusaxl.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">brooker.co.za/misc-blog/2024/0</span><span class="invisible">7/07/prusaxl.html</span></a></p>
Marc Brooker<p>A very nice way to spend an afternoon.</p>
Marc Brooker<p>New blog post, on the &quot;you don&#39;t need distributed systems&quot; meme, and the idea that distributed systems are only about scale: <a href="https://brooker.co.za/blog/2024/06/04/scale.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">brooker.co.za/blog/2024/06/04/</span><span class="invisible">scale.html</span></a> </p><p>Short version: scale is only a tiny part of what makes distributed systems interesting and useful.</p>
Marc Brooker<p>Why is it considered totally normal to live places where heating is required to stay alive, but some kind of affront to nature to live places where cooling is required to stay alive?</p>
Marc Brooker<p>Ignore the clickbait title, this is fascinating. It goes to show how much we lose when we collapse the full spectrum of color down to a 3-vector.</p><p><a href="https://www.youtube.com/watch?v=UQuIVsNzqDk" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=UQuIVsNzqD</span><span class="invisible">k</span></a></p><p>We make color a 3-vector (or a 4-vector) because that&#39;s how our color perception works. But it&#39;s not how color physically works. It throws out a vast amount of spectral information (not to mention the phase information).</p>
Marc Brooker<p><span class="h-card" translate="no"><a href="https://mastodon.social/@ltratt" class="u-url mention">@<span>ltratt</span></a></span> My believe on why UML never really succeeded is that it doesn&#39;t do this well. It&#39;s on the wrong semantic level to specify the known-knowns about behavior, and to explore the unknown about structure or behavior. Too high level for one, too low for another.</p>
Marc Brooker<p><span class="h-card" translate="no"><a href="https://mastodon.social/@ltratt" class="u-url mention">@<span>ltratt</span></a></span> <br />Good software practices, and mature teams, both take maximal advantage of the things they know to reduce iteration, and use iteration as a tool for discovering the things they don&#39;t know. They&#39;re curious, and expand the set of things they know from experience (theirs and others).</p>
Marc Brooker<p><span class="h-card" translate="no"><a href="https://mastodon.social/@ltratt" class="u-url mention">@<span>ltratt</span></a></span> What we should be embarrassed about is unneeded iteration: cases where we wastefully iterate towards goals that are well-known and can be clearly specified. This is a big part of my interest in tools like P and TLA+: going &quot;direct to goal&quot; for the well-understood problems.</p>
Marc Brooker<p>This is smart stuff from <span class="h-card" translate="no"><a href="https://mastodon.social/@ltratt" class="u-url mention">@<span>ltratt</span></a></span> I might go further and say that the ability to iterate at relatively low cost is one of the defining benefits of software, and not something we need to be embarrassed about: <a href="https://tratt.net/laurie/blog/2024/what_factors_explain_the_nature_of_software.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">tratt.net/laurie/blog/2024/wha</span><span class="invisible">t_factors_explain_the_nature_of_software.html</span></a></p>
Marc Brooker
Marc Brooker<p>New blog post, about Nagle&#39;s algorithm and TCP_NODELAY: <a href="https://brooker.co.za/blog/2024/05/09/nagle.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">brooker.co.za/blog/2024/05/09/</span><span class="invisible">nagle.html</span></a></p><p>In the post, I look into the history of Nagle&#39;s algorithm, the interaction with delayed ack, and propose that it&#39;s not the right default for the modern internet.</p>
ExploreLive feeds
About