Language Selection

English French German Italian Portuguese Spanish

Mozilla on Synthesizing Loop-Free Programs with Rust and Z3 and on Privacy

Filed under
Development
Moz/FF
  • Synthesizing Loop-Free Programs with Rust and Z3

    Automatically finding a program that implements a given specification is called program synthesis. The main difficulty is that the search space is huge: the number of programs of size \(n\) grows exponentially. Naïvely enumerating every program of size \(n\), checking whether each one satisfies the specification, and then moving on to programs of size \(n+1\) and so on doesn’t scale. However, the field has advanced by using smarter search techniques to prune the search space, leveraging performance improvements in SMT solvers, and at times limiting the scope of the problem.

    In this post, I’ll explain one approach to modern program synthesis: counterexample-guided iterative synthesis of component-based, loop-free programs, as described in Synthesis of Loop-Free Programs by Gulwani et al. We’ll dissect exactly what each of those terms mean, and we’ll also walk through an implementation written in Rust that uses the Z3 solver.

  • No judgment digital definitions: Online advertising strategies

    It’s hard to go anywhere on the internet without seeing an ad. That’s because advertising is the predominant business model of the internet today. Websites and apps you visit every day are largely “free” for you because they monetize your data and your attention through advertising. And, as data sets of individuals and groups online have become more readily available to companies in recent years, advertisers have developed strategies to minimize what they spend on ads while maximizing the profit made from them. The ad tech arms race is constantly evolving, and the more invasive practices that are used, the more valuable your data is. Here are some of the most common online advertising strategies and associated activities being used that rely on collecting data about you today.

More in Tux Machines

7 Linux Distros to Look Forward in 2021

Here is a list of most anticipated Linux distributions you should keep an eye on in the year 2021. Read more

Games Leftovers

  • Gaming Like It's 1925: Last Week To Join The Public Domain Game Jam!

    Sign up for the Public Domain Game Jam on itch.io »

  • ujoy(4) added to -current

    With the following commit, Thomas Frohwein (thfr@) added a joystick/gamecontroller driver to -current: [...]

  • The First Online Conference Is Happening Today For The Godot Game Engine - Phoronix

    For those interested in Godot as the premiere open-source 2D/3D game engine or just looking for some interesting technical talks to enjoy this weekend, the first GodotCon Online is today. GodotCon 2021 is the open-source game engine's first entirely online conference for developers, users, and other contributors to this promising open-source project. The YouTube-based event has been running from 8:45 UTC today until 16:00 UTC, but fear not if you missed out as you can already go back and listen to the prior talks in the stream. The recordings will remain available for those wanting to enjoy it in the days ahead. All of the content is free of charge.

Programming Leftovers

  • How to test PHP code using PHPUnit - Anto ./ Online

    PHPUnit automatically executable tests that verify your application’s behavior. Thus – you can ensure that your changes don’t break existing functionality. This post will show you how to test your PHP code using PHPUnit.

  • Latency Numbers Every Team Should Know

    We design systems around the size of delays that are expected. You may have seen the popular table “latency numbers every programmer should know” which lists some delays that are significant in technology systems we build. Teams are systems too. Delays in operations that teams need to perform regularly are significant to their effectiveness. We should know what they are. Ssh to a server on the other side of the world and you will feel frustration; delay in the feedback loop from keypress to that character displayed on the screen. Here’s some important feedback loops for a team, with feasible delays. I’d consider these delays tolerable by a team doing their best work (in contexts I’ve worked in). Some teams can do better, lots do worse. [...] In recent times you may have experienced the challenge of having conversations over video links with significant delays. This is even harder when the delay is variable. It’s hard to avoid talking over each other. Similarly, it’s pretty bad if we know it’s going to take all day to deploy a change to production. But it’s so worse if we think we can do it in 10 minutes, when it actually ends up taking all day. Flaky deployment checks, environment problems, change conflicts create unpredictable delays. It’s hard to get anything done when we don’t know what to expect. Like trying to hold a video conversation with someone on a train that’s passing through the occasional tunnel.

  • How I programmed a virtual gift exchange

    Every year, my wife's book club has a book exchange during the holidays. Due to the need to maintain physical distance in 2020, I created an online gift exchange for them to use during a book club videoconference. Apparently, the virtual book exchange worked out (at least, I received kind compliments from the book club members), so I decided to share this simple little hack.

  • Dirk Eddelbuettel: prrd 0.0.4: More tweaks

    The key idea of prrd is simple, and described in some more detail on its webpage and its GitHub repo. Reverse dependency checks are an important part of package development that is easily done in a (serial) loop. But these checks are also generally embarassingly parallel as there is no or little interdependency between them (besides maybe shared build depedencies). See the (dated) screenshot (running six parallel workers, arranged in split byobu session). This release brings several smaller tweaks and improvements to the summary report that had accumulated in my use since the last release last April. We also updated the CI runners as one does these days.

  • vrurg: A New Release Of Cro::RPC::JSON

    I don’t usually announce regular releases of my modules. But not this time. I start this new year with the new v0.1 branch of Cro::RPC::JSON. Version 0.1.1 is currently available on CPAN (will likely be replaced with fez as soon as it is ready). The release is a result of so extensive changes in the module that I had to bump its :api version to 2.

  • gfldex: Anonymous slurpers

    I have a script where I’m only interested in the last two lines of its output.

Nouveau X.Org Driver Sees First Release In Two Years

Two years and nine patches later, xf86-video-nouveau 1.0.17 is out as the latest X.Org driver update for this open-source NVIDIA driver component. Like the other DDX drivers with the exception of the generic xf86-video-modesetting driver that is quite common now to those still running on X.Org with the open-source stack, xf86-video-nouveau seldom sees new activity. Since the prior v1.0.16 release two years ago there has been less than a dozen patches for it. The interesting activity happens in DRM/KMS kernel space and an increasing number of users are just relying upon xf86-video-modesetting over these hardware-specific X.Org user-space drivers. Read more