The Unclear Impact

Krist贸f Marussy ferdium馃巰 | @kristof@pleroma.marussy.com

I'm a PhD student working on the extra-functional requirements and formal verification of cyber-physical system architectures.
I also like free (as in liberty) software, privacy enhancing technologies, and cryptography.

I may not be trans but transgender hating script kiddies are too incompetent to tell the difference. Donkey Kong says trans rights = human rights.

a general purpose computer where you can鈥檛 replace microsoft鈥檚 root of trust keys with yours isn鈥檛 general purpose

vb.net

@tindall that鈥檚 not a type of guy, that鈥檚 a Guy(Of type) blobfoxcomputerowo

@juliank @juliank ah, thanks! very interesting

I never realized apt was allowed reshuffle already (automatically) installed packages, but in that case, stability sounds useful indeed blobfoxcomfy

@juliank btw (I am not very familiar with apt, so pardon me if this is nonsense), how large/difficult are these dependency resolution problems that you need a custom decision procedure for them? naively, directly encoding everything into SAT seems possible

(OTOH p2 in Eclipse does just that, and is usually dreadfully slow)

@juliank the parallel exploration on different parts of the graph sounds a bit weird for me at first. in the end, you鈥檇 need to integrate the results from multiple threads, where the nodes could have shifted around in different ways.

a simpler approach could be to explore different parts of the search space in parallel: say, pick an initial branching point, and explore the possible outcomes (selected node in the or-group in your case) in separate threads. however, this may need more memory to keep track of each candidate solution on each threads (but persistent data structures with structural sharing can reduce the overhead considerably)

@juliank we鈥檙e trying to generate large(-ish) graphs which satisfy some first-order constraints (useful as test inputs or design space exploration), so we have the benefit that our graph starts small and grows big as the solver runs 鈥 it seems you鈥檙e having to deal with the opposite blobfoxupsidedown

but I鈥檒l try to keep this use-case in mind 鈥 the very least, now I know that I could make nice graph-processing benchmarks from apt install :)

clause learning seems quite hard in this space, because the nodes of the graph 鈥榮hift鈥 around as you are merging them (we鈥檙e doing the opposite by splitting), so there is no easy way to generalize the results of conflict analysis into a lemma鈥

data structures, long

@juliank at uni, we鈥檙e developing something similar (in java, however), for SAT solving actually

in a previous version of the system, we were basically using journaling. that makes backtracking relatively easy, but jumping across different branches of the derivation tree (e.g., some heuristic tells you to abandon whatever you were doing, try something else, but if that doesn鈥檛 yield a solution quickly, go back to wherever you were in the search space) become inefficient, because you always have to first go back to the common ancestor, and then drill down again

currently, we鈥檙e experimenting with persistent data structures. HAMTs seem to work nicely as a big collection of labeled tuples (~graph edges). we鈥檙e following this paper: https://michael.steindorfer.name/publications/oopsla15.pdf but implemented it from scratch with our own optimizations

one particular optimization that seems useful is to have immutable and mutable tree nodes, and 鈥渃heck in鈥 a new revision of a collection by copying each mutable node into a packed immutable one, which can handle batch updates more efficiently (immutable -> mutable when performing an update is just CoW)

of course, a persistent set of tuples is barely a graph, so we also have to maintain indexes for adjacency. the cool thing is that it鈥檚 very fast to determine the delta between two persistent data structures (just iterate over the two trees, skipping over immutable nodes that are referentially identical): when backtracking, you can calculate a delta (usually small), and update (mutable) indexes accordingly. we鈥檙e using https://github.com/viatra/org.eclipse.viatra to incrementally maintain indexes and graph queries, but https://github.com/vmware/differential-datalog would be another alternative

another idea would be to use another persistent data structure, like a ROMDD, radix tree, or even B-tree to store the indexes. but that might lead to pathological behavior on some inputs (that a randomly selected hash function in HAMT can avoid)

w.r.t. doing this in native code, I think you could get away with just releasing all mutable nodes when 鈥渃hecking in鈥 and never releasing immutable ones (since 鈥渃hecking in鈥 can control the number of stored versions, hopefully, there won鈥檛 be extremely many). otherwise, I鈥檇 try adding a refcount to mutable nodes, but I have no idea about its efficiency

academia
It was 3 blobfoxuwu

academia

optional author response period only to those papers which reached some level of support

does the lack of questions to respond to mean that

  1. my paper was outright rejected with no support at all
  2. the reviewers liked the paper, but had no questions
  3. the chairs are late with sending out the questions

rationally, 3. is overwhelmingly likely, but my anxiety is mounting about 1. blobfoxteaterrified

making it clear that outright rejected papers will be notified early would have been nice

i guess i have now learn about pleroma federating chats across instances. cool blobfoxuwu

@retronav @yarmo stripe offers a profiling service, ostensibly for fraud prevention: https://stripe.com/radar their checkout product integrates with that: https://stripe.com/payments/checkout (see the Powerful fraud prevention section)

it鈥檚 baffling why do they think it鈥檚 okay to profile users, especially those who aren鈥檛 participating in any monetary transactions (not as if profiling paying customers would be less fishy, but at least they鈥檇 have the fraud prevention leg to stand on)

finally, no x11 clients blobfoxuwu

Re: self-driving cars, accidents

@szakib @trisschen @rysiek @cassidymcgurk given the stringent standards for certifying safety-critical systems (even in the automotive domain, where cost savings are otherwise foremost), this is not surprising: it鈥檚 highly unlikely one could devise a way to demonstrate the safety of an autopilot-like system with current system architectures

which, in a sane world, would mean deploying no such systems in production at all

Re: self-driving cars, accidents

@rysiek @cassidymcgurk what is weird is that how come disengaging not an admission that decisions made by the self-driving component up to that point have lead to an unsafe situtation? like we鈥檇 expect a human driver to drive defensively and not intentionally get into a dangerous situation

(test cases and even whole methods to generate such test cases have been proposed in academic literature as well as by some industry players, e.g., to make sure the system can reason about potential object obscured from its vision. so there鈥檚 at least an expectation for self-driving components to be programmed this way. nevertheless, tesla 鈥 and i presume other implementers 鈥 chose the easy way out and blame humans for the shortcomings of their systems)

got greeted by a kernel panic during early userspace after updating my system and reboot. how rude!

seems to have been resolved after a power cycle, for some reason

@be i vaguely recall playing with a GCC extension in some homework at uni that allows you to make a template <typename Char, Char... Xs> operator""_ and takes the characters of the literal for you to metaprogram with. (for reasons, i implemented a recursive descent parser as a template metaprogram that makes the type of the string literal vary based on the contents of the literal blobfoxcomputerowo )

my homework had -Wgnu-string-literal-operator-template in it to compile with clang++, but I can鈥檛 find anything about that in current docs

hopefully, the lack of docs means that this extension never got standardized

late stage capitalism

whelp, i can鈥檛 exactly delete my github account right now (need it for uni stuff), but the pointless achievements they introduced is as good as a reason as any to at least set my profile completely private (and hide the achievements!)

@paullammers @Sylvhem masking systemd units is the standard way to make sure a service is not started by any kind of activation (as opposed to disabling, which just makes sure it is not started automatically), so it鈥檚 not that ridiculous to propose as a fix. the binaries and libraries are still in place (I presume they are a mandatory dependency of gnome because it uses some stuff from some libraries), but systemd will refuse to start the corresponding user unit

what is more ridiculous is that gnome insist on activating the tracker service even when it is disabled

@aral i found using a rectangle the matches the color of the underlying text somewhat (instead of pure black) can be an aesthetic solution while still being reasonable secure, especially for text with a dark theme (where a black rectangle would just completely disappear)

i wonder how hard would it be to automate that 鈥 perhaps quantizing the color to a small palette, to avoid disclosing information through quirks in the color auto-detection algorithm

Re: shitpost, pol

@robby @signal9 the beatings will continue until the ethernet is plugged back blobfoxoutage